theories/compile.v

@@ -0,0 +1,136 @@
+Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax fp_red.
+Require Import ssreflect ssrbool.
+From Hammer Require Import Tactics.
+
+Module Compile.
+  Fixpoint F {n} (a : Tm n) : Tm n :=
+    match a with
+    | TBind p A B => Pair (Pair (Const p) (F A)) (Abs (F B))
+    | Const k => Const k
+    | Univ i => Univ i
+    | Abs a => Abs (F a)
+    | App a b => App (F a) (F b)
+    | VarTm i => VarTm i
+    | Pair a b => Pair (F a) (F b)
+    | Proj t a => Proj t (F a)
+    end.
+
+  Lemma renaming n m (a : Tm n) (ξ : fin n -> fin m) :
+    F (ren_Tm ξ a)= ren_Tm ξ (F a).
+  Proof. move : m ξ. elim : n  / a => //=; scongruence. Qed.
+
+  #[local]Hint Rewrite Compile.renaming : compile.
+
+  Lemma morphing n m (a : Tm n) (ρ0 ρ1 : fin n -> Tm m) :
+    (forall i, ρ0 i = F (ρ1 i)) ->
+    subst_Tm ρ0 (F a) = F (subst_Tm ρ1 a).
+  Proof.
+    move : m ρ0 ρ1. elim : n / a => n//=.
+    - hauto lq:on inv:option rew:db:compile unfold:funcomp.
+    - hauto lq:on rew:off.
+    - hauto lq:on rew:off.
+    - hauto lq:on.
+    - hauto lq:on inv:option rew:db:compile unfold:funcomp.
+  Qed.
+
+  Lemma substing n b (a : Tm (S n)) :
+    subst_Tm (scons (F b) VarTm) (F a) = F (subst_Tm (scons b VarTm) a).
+  Proof.
+    apply morphing.
+    case => //=.
+  Qed.
+
+End Compile.
+
+#[export] Hint Rewrite Compile.renaming Compile.morphing : compile.
+
+
+Module Join.
+  Definition R {n} (a b : Tm n) := join (Compile.F a) (Compile.F b).
+
+  Lemma BindInj n p0 p1 (A0 A1 : Tm n) B0 B1  :
+    R (TBind p0 A0 B0) (TBind p1 A1 B1) -> p0 = p1 /\ R A0 A1 /\ R B0 B1.
+  Proof.
+    rewrite /R /= !join_pair_inj.
+    move => [[/join_const_inj h0 h1] h2].
+    apply abs_eq in h2.
+    evar (t : Tm (S n)).
+    have : join (App (ren_Tm shift (Abs (Compile.F B1))) (VarTm var_zero)) t by
+      apply Join.FromPar; apply Par.AppAbs; auto using Par.refl.
+    subst t. rewrite -/ren_Tm.
+    move : h2. move /join_transitive => /[apply]. asimpl => h2.
+    tauto.
+  Qed.
+
+  Lemma UnivInj n i j : R (Univ i : Tm n) (Univ j) -> i = j.
+  Proof. hauto l:on use:join_univ_inj. Qed.
+
+End Join.
+
+Module Equiv.
+  Inductive R {n} : Tm n -> Tm n ->  Prop :=
+  (***************** Beta ***********************)
+  | AppAbs a b :
+    R (App (Abs a) b)  (subst_Tm (scons b VarTm) a)
+  | ProjPair p a b :
+    R (Proj p (Pair a b)) (if p is PL then a else b)
+
+  (****************** Eta ***********************)
+  | AppEta a :
+    R a (Abs (App (ren_Tm shift a) (VarTm var_zero)))
+  | PairEta a :
+    R a (Pair (Proj PL a) (Proj PR a))
+
+  (*************** Congruence ********************)
+  | Var i : R (VarTm i) (VarTm i)
+  | AbsCong a b :
+    R a b ->
+    R (Abs a) (Abs b)
+  | AppCong a0 a1 b0 b1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R (App a0 b0) (App a1 b1)
+  | PairCong a0 a1 b0 b1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R (Pair a0 b0) (Pair a1 b1)
+  | ProjCong p a0 a1 :
+    R a0 a1 ->
+    R (Proj p a0) (Proj p a1)
+  | BindCong p A0 A1 B0 B1:
+    R A0 A1 ->
+    R B0 B1 ->
+    R (TBind p A0 B0) (TBind p A1 B1)
+  | UnivCong i :
+    R (Univ i) (Univ i).
+End Equiv.
+
+Module EquivJoin.
+  Lemma FromEquiv n (a b : Tm n) : Equiv.R a b -> Join.R a b.
+  Proof.
+    move => h. elim : n a b /h => n.
+    - move => a b.
+      rewrite /Join.R /join /=.
+      eexists. split. apply relations.rtc_once.
+      apply Par.AppAbs; auto using Par.refl.
+      rewrite Compile.substing.
+      apply relations.rtc_refl.
+    - move => p a b.
+      apply Join.FromPar.
+      simpl. apply : Par.ProjPair'; auto using Par.refl.
+      case : p => //=.
+    - move => a. apply Join.FromPar => /=.
+      apply : Par.AppEta'; auto using Par.refl.
+      by autorewrite with compile.
+    - move => a. apply Join.FromPar => /=.
+      apply : Par.PairEta; auto using Par.refl.
+    - hauto l:on use:Join.FromPar, Par.Var.
+    - hauto lq:on use:Join.AbsCong.
+    - qauto l:on use:Join.AppCong.
+    - qauto l:on use:Join.PairCong.
+    - qauto use:Join.ProjCong.
+    - rewrite /Join.R => p A0 A1 B0 B1 _ hA _ hB /=.
+      sfirstorder use:Join.PairCong,Join.AbsCong,Join.FromPar,Par.ConstCong.
+    - hauto l:on.
+  Qed.
+End EquivJoin.

theories/fp_red.v

@@ -410,16 +410,16 @@ Module RPar.
     qauto l:on ctrs:R inv:option.
   Qed.
 
-  Lemma var_or_bot_imp {n} (a b : Tm n) :
-    var_or_bot a ->
-    a = b -> ~~ var_or_bot b -> False.
+  Lemma var_or_const_imp {n} (a b : Tm n) :
+    var_or_const a ->
+    a = b -> ~~ var_or_const b -> False.
   Proof.
     hauto lq:on inv:Tm.
   Qed.
 
-  Lemma var_or_bot_up n m (ρ : fin n -> Tm m) :
-    (forall i, var_or_bot (ρ i)) ->
-    (forall i, var_or_bot (up_Tm_Tm ρ i)).
+  Lemma var_or_const_up n m (ρ : fin n -> Tm m) :
+    (forall i, var_or_const (ρ i)) ->
+    (forall i, var_or_const (up_Tm_Tm ρ i)).
   Proof.
     move => h /= [i|].
     - asimpl.
@@ -430,10 +430,10 @@ Module RPar.
     - sfirstorder.
   Qed.
 
-  Local Ltac antiimp := qauto l:on use:var_or_bot_imp.
+  Local Ltac antiimp := qauto l:on use:var_or_const_imp.
 
   Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) :
-    (forall i, var_or_bot (ρ i)) ->
+    (forall i, var_or_const (ρ i)) ->
     R (subst_Tm ρ a) b -> exists b0, R a b0 /\ subst_Tm ρ b0 = b.
   Proof.
     move E : (subst_Tm ρ a) => u hρ h.
@@ -444,7 +444,7 @@ Module RPar.
       case : c => //=; first by antiimp.
       move => c [?]. subst.
       spec_refl.
-      have /var_or_bot_up hρ' := hρ.
+      have /var_or_const_up hρ' := hρ.
       move : iha hρ' => /[apply] iha.
       move : ihb hρ => /[apply] ihb.
       spec_refl.
@@ -470,7 +470,7 @@ Module RPar.
     - move => n p a0 a1 ha iha m ρ hρ []//=;
                first by antiimp.
       move => p0 []//= t [*]; first by antiimp. subst.
-      have  /var_or_bot_up {}/iha  := hρ => iha.
+      have  /var_or_const_up {}/iha  := hρ => iha.
       spec_refl. move : iha => [b0 [? ?]]. subst.
       eexists. split. apply ProjAbs; eauto. by asimpl.
     - move => n p a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=;
@@ -488,7 +488,7 @@ Module RPar.
       hauto l:on.
     - move => n a0 a1 ha iha m ρ hρ []//=; first by antiimp.
       move => t [*]. subst.
-      have /var_or_bot_up {}/iha := hρ => iha.
+      have /var_or_const_up {}/iha := hρ => iha.
       spec_refl.
       move  :iha => [b0 [? ?]]. subst.
       eexists. split. by apply AbsCong; eauto.
@@ -524,7 +524,7 @@ Module RPar.
                first by antiimp.
       move => ? t t0 [*]. subst.
       have {}/iha := (hρ) => iha.
-      have /var_or_bot_up {}/ihB := (hρ) => ihB.
+      have /var_or_const_up {}/ihB := (hρ) => ihB.
       spec_refl.
       move : iha => [b0 [? ?]].
       move : ihB => [c0 [? ?]]. subst.
@@ -1838,7 +1838,7 @@ Definition prov_extract_spec {n} u (a : Tm n) :=
   | TBind p A B => exists A0 B0, extract a = TBind p A0 B0 /\ rtc Par.R A A0 /\ rtc Par.R B B0
   | Univ i => extract a = Univ i
   | VarTm i => extract a = VarTm i
-  | (Const TPi) => extract a = (Const TPi)
+  | (Const i) => extract a = (Const i)
   | _ => True
   end.
 
@@ -2250,6 +2250,15 @@ Proof.
   apply prov_extract.
 Qed.
 
+Lemma pars_const_inv n i (c : Tm n) :
+  rtc Par.R (Const i) c ->
+  extract c = Const i.
+Proof.
+  have : prov (Const i) (Const i : Tm n) by sfirstorder.
+  move : prov_pars. repeat move/[apply].
+  apply prov_extract.
+Qed.
+
 Lemma pars_pi_inv n p (A : Tm n) B C :
   rtc Par.R (TBind p A B) C ->
   exists A0 B0, extract C = TBind p A0 B0 /\
@@ -2277,6 +2286,14 @@ Proof.
   sauto l:on use:pars_univ_inv.
 Qed.
 
+Lemma pars_const_inj n i j (C : Tm n) :
+  rtc Par.R (Const i) C ->
+  rtc Par.R (Const j) C ->
+  i = j.
+Proof.
+  sauto l:on use:pars_const_inv.
+Qed.
+
 Lemma pars_pi_inj n p0 p1 (A0 A1 : Tm n) B0 B1 C :
   rtc Par.R (TBind p0 A0 B0) C ->
   rtc Par.R (TBind p1 A1 B1) C ->
@@ -2314,6 +2331,12 @@ Proof.
   sfirstorder use:pars_univ_inj.
 Qed.
 
+Lemma join_const_inj n i j :
+  join (Const i : Tm n) (Const j) -> i = j.
+Proof.
+  sfirstorder use:pars_const_inj.
+Qed.
+
 Lemma join_pi_inj n p0 p1 (A0 A1 : Tm n) B0 B1 :
   join (TBind p0 A0 B0) (TBind p1 A1 B1) ->
   p0 = p1 /\ join A0 A1 /\ join B0 B1.