Minor

theories/common.v

@@ -60,6 +60,7 @@ Fixpoint ishne {n} (a : PTm n) :=
   | VarPTm _ => true
   | PApp a _ => ishne a
   | PProj _ a => ishne a
+  | PBot => true
   | _ => false
   end.
 
@@ -90,3 +91,7 @@ Proof. case : a => //=. Qed.
 Definition ispair_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
   ispair (ren_PTm ξ a) = ispair a.
 Proof. case : a => //=. Qed.
+
+Definition ishne_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
+  ishne (ren_PTm ξ a) = ishne a.
+Proof. move : m ξ. elim : n / a => //=. Qed.

theories/fp_red.v

@@ -20,7 +20,7 @@ Ltac2 spec_refl () :=
                try (specialize $h with (1 := eq_refl))
            end)  (Control.hyps ()).
 
-Ltac spec_refl := ltac2:(spec_refl ()).
+Ltac spec_refl := ltac2:(Control.enter spec_refl).
 
 Module EPar.
   Inductive R {n} : PTm n -> PTm n ->  Prop :=
@@ -262,6 +262,12 @@ end.
 Lemma ne_nf n a : @ne n a -> nf a.
 Proof. elim : a => //=. Qed.
 
+Lemma ne_nf_ren n m (a : PTm n) (ξ : fin n -> fin m) :
+  (ne a <-> ne (ren_PTm ξ a)) /\ (nf a <-> nf (ren_PTm ξ a)).
+Proof.
+  move : m ξ. elim : n / a => //=; solve [hauto b:on].
+Qed.
+
 Inductive TRedSN' {n} (a : PTm n) : PTm n -> Prop :=
 | T_Refl :
   TRedSN' a a
@@ -293,6 +299,12 @@ Proof.
   apply N_β'. by asimpl. eauto.
 Qed.
 
+Lemma ne_nf_embed n (a : PTm n) :
+  (ne a -> SNe a) /\ (nf a -> SN a).
+Proof.
+  elim : n  / a => //=; hauto qb:on ctrs:SNe, SN.
+Qed.
+
 #[export]Hint Constructors SN SNe TRedSN : sn.
 
 Ltac2 rec solve_anti_ren () :=
@@ -836,12 +848,6 @@ Module RReds.
 End RReds.
 
 
-Lemma ne_nf_ren n m (a : PTm n) (ξ : fin n -> fin m) :
-  (ne a <-> ne (ren_PTm ξ a)) /\ (nf a <-> nf (ren_PTm ξ a)).
-Proof.
-  move : m ξ. elim : n / a => //=; solve [hauto b:on].
-Qed.
-
 Module NeEPar.
   Inductive R_nonelim {n} : PTm n -> PTm n ->  Prop :=
   (****************** Eta ***********************)
@@ -1440,6 +1446,14 @@ Module ERed.
     all : hauto lq:on ctrs:R.
   Qed.
 
+  Lemma nf_preservation n (a b : PTm n) :
+    ERed.R a b -> (nf a -> nf b) /\ (ne a -> ne b).
+  Proof.
+    move => h.
+    elim : n a b /h => //=;
+                        hauto lqb:on use:ne_nf_ren,ne_nf.
+  Qed.
+
 End ERed.
 
 Module EReds.
@@ -1510,10 +1524,70 @@ Module EReds.
     induction 1; hauto lq:on ctrs:rtc use:ERed.substing.
   Qed.
 
+  Lemma app_inv n (a0 b0 C : PTm n) :
+    rtc ERed.R (PApp a0 b0) C ->
+    exists a1 b1, C = PApp a1 b1 /\
+               rtc ERed.R a0 a1 /\
+               rtc ERed.R b0 b1.
+  Proof.
+    move E : (PApp a0 b0) => u hu.
+    move : a0 b0 E.
+    elim : u C / hu.
+    - hauto lq:on ctrs:rtc.
+    - move => a b c ha ha' iha a0 b0 ?. subst.
+      hauto lq:on rew:off ctrs:rtc, ERed.R inv:ERed.R.
+  Qed.
+
+  Lemma proj_inv n p (a C : PTm n) :
+    rtc ERed.R (PProj p a) C ->
+    exists c, C = PProj p c /\ rtc ERed.R a c.
+  Proof.
+    move E : (PProj p a) => u hu.
+    move : p a E.
+    elim : u C /hu;
+      hauto q:on ctrs:rtc,ERed.R inv:ERed.R.
+  Qed.
+
+  Lemma bind_inv n p (A : PTm n) B C :
+    rtc ERed.R (PBind p A B) C ->
+    exists A0 B0, C = PBind p A0 B0 /\ rtc ERed.R A A0 /\ rtc ERed.R B B0.
+  Proof.
+    move E : (PBind p A B) => u hu.
+    move : p A B E.
+    elim : u C / hu.
+    hauto lq:on ctrs:rtc.
+    hauto lq:on rew:off ctrs:rtc, ERed.R inv:ERed.R, rtc.
+  Qed.
+
 End EReds.
 
 #[export]Hint Constructors ERed.R RRed.R EPar.R : red.
 
+Module EJoin.
+  Definition R {n} (a b : PTm n) := exists c, rtc ERed.R a c /\ rtc ERed.R b c.
+
+  Lemma hne_app_inj n (a0 b0 a1 b1 : PTm n) :
+    R (PApp a0 b0) (PApp a1 b1) ->
+    R a0 a1 /\ R b0 b1.
+  Proof.
+    hauto lq:on use:EReds.app_inv.
+  Qed.
+
+  Lemma hne_proj_inj n p0 p1 (a0 a1 : PTm n) :
+    R (PProj p0 a0) (PProj p1 a1) ->
+    p0 = p1 /\ R a0 a1.
+  Proof.
+    hauto lq:on rew:off use:EReds.proj_inv.
+  Qed.
+
+  Lemma bind_inj n p0 p1 (A0 A1 : PTm n) B0 B1 :
+    R (PBind p0 A0 B0) (PBind p1 A1 B1) ->
+    p0 = p1 /\ R A0 A1 /\ R B0 B1.
+  Proof.
+    hauto lq:on rew:off use:EReds.bind_inv.
+  Qed.
+
+End EJoin.
 
 Module RERed.
   Inductive R {n} : PTm n -> PTm n ->  Prop :=
@@ -1602,9 +1676,17 @@ Module RERed.
     hauto q:on use:ToBetaEta, FromBeta, FromEta, RRed.substing, ERed.substing.
   Qed.
 
+  Lemma hne_preservation n (a b : PTm n) :
+    RERed.R a b -> ishne a -> ishne b.
+  Proof.  induction 1; sfirstorder. Qed.
+
 End RERed.
 
 Module REReds.
+  Lemma hne_preservation n (a b : PTm n) :
+    rtc RERed.R a b -> ishne a -> ishne b.
+  Proof.  induction 1; eauto using RERed.hne_preservation, rtc_refl, rtc. Qed.
+
   Lemma sn_preservation n (a b : PTm n) :
     rtc RERed.R a b ->
     SN a ->
@@ -1686,6 +1768,40 @@ Module REReds.
     hauto lq:on rew:off ctrs:rtc inv:RERed.R.
   Qed.
 
+  Lemma var_inv n (i : fin n) C :
+    rtc RERed.R (VarPTm i) C ->
+    C = VarPTm i.
+  Proof.
+    move E : (VarPTm i) => u hu.
+    move : i E. elim : u C /hu; hauto lq:on rew:off inv:RERed.R.
+  Qed.
+
+  Lemma hne_app_inv n (a0 b0 C : PTm n) :
+    rtc RERed.R (PApp a0 b0) C ->
+    ishne a0 ->
+    exists a1 b1, C = PApp a1 b1 /\
+               rtc RERed.R a0 a1 /\
+               rtc RERed.R b0 b1.
+  Proof.
+    move E : (PApp a0 b0) => u hu.
+    move : a0 b0 E.
+    elim : u C / hu.
+    - hauto lq:on ctrs:rtc.
+    - move => a b c ha ha' iha a0 b0 ?. subst.
+      hauto lq:on rew:off ctrs:rtc, RERed.R use:RERed.hne_preservation inv:RERed.R.
+  Qed.
+
+  Lemma hne_proj_inv n p (a C : PTm n) :
+    rtc RERed.R (PProj p a) C ->
+    ishne a ->
+    exists c, C = PProj p c /\ rtc RERed.R a c.
+  Proof.
+    move E : (PProj p a) => u hu.
+    move : p a E.
+    elim : u C /hu;
+      hauto q:on ctrs:rtc,RERed.R use:RERed.hne_preservation inv:RERed.R.
+  Qed.
+
   Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
     rtc RERed.R a b -> rtc RERed.R (subst_PTm ρ a) (subst_PTm ρ b).
   Proof.
@@ -1721,6 +1837,14 @@ Module REReds.
     hauto l:on use:substing.
   Qed.
 
+  Lemma ToEReds n (a b : PTm n) :
+    nf a ->
+    rtc RERed.R a b -> rtc ERed.R a b.
+  Proof.
+    move => + h.
+    induction h; hauto lq:on rew:off ctrs:rtc use:RERed.ToBetaEta, RReds.nf_refl, @rtc_once, ERed.nf_preservation.
+  Qed.
+
 End REReds.
 
 Module LoRed.
@@ -1776,6 +1900,22 @@ Module LoRed.
     RRed.R a b.
   Proof. induction 1; hauto lq:on ctrs:RRed.R. Qed.
 
+  Lemma AppAbs' n a (b : PTm n) u :
+    u = (subst_PTm (scons b VarPTm) a) ->
+    R (PApp (PAbs a) b)  u.
+  Proof. move => ->. apply AppAbs. Qed.
+
+  Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
+    R a b -> R (ren_PTm ξ a) (ren_PTm ξ b).
+  Proof.
+    move => h. move : m ξ.
+    elim : n a b /h.
+
+    move => n a b m ξ /=.
+    apply AppAbs'. by asimpl.
+    all : try qauto ctrs:R use:ne_nf_ren, ishf_ren.
+  Qed.
+
 End LoRed.
 
 Module LoReds.
@@ -2107,6 +2247,12 @@ Module DJoin.
   Lemma refl n (a : PTm n) : R a a.
   Proof. sfirstorder use:@rtc_refl unfold:R. Qed.
 
+  Lemma FromEJoin n (a b : PTm n) : EJoin.R a b -> DJoin.R a b.
+  Proof. hauto q:on use:REReds.FromEReds. Qed.
+
+  Lemma ToEJoin n (a b : PTm n) : nf a -> nf b -> DJoin.R a b -> EJoin.R a b.
+  Proof. hauto q:on use:REReds.ToEReds. Qed.
+
   Lemma symmetric n (a b : PTm n) : R a b -> R b a.
   Proof. sfirstorder unfold:R. Qed.
 
@@ -2180,6 +2326,17 @@ Module DJoin.
     case : c => //=; itauto.
   Qed.
 
+  Lemma hne_univ_noconf n (a b : PTm n) :
+    R a b -> ishne a -> isuniv b -> False.
+  Proof.
+    move => [c [h0 h1]] h2 h3.
+    have {h0 h1 h2 h3} : ishne c /\ isuniv c by
+      hauto l:on use:REReds.hne_preservation,
+          REReds.univ_preservation.
+    move => [].
+    case : c => //=.
+  Qed.
+
   Lemma bind_inj n p0 p1 (A0 A1 : PTm n) B0 B1 :
     DJoin.R (PBind p0 A0 B0) (PBind p1 A1 B1) ->
     p0 = p1 /\ DJoin.R A0 A1 /\ DJoin.R B0 B1.
@@ -2188,12 +2345,34 @@ Module DJoin.
     hauto lq:on rew:off use:REReds.bind_inv.
   Qed.
 
+  Lemma var_inj n (i j : fin n) :
+    R (VarPTm i) (VarPTm j) -> i = j.
+  Proof. sauto lq:on rew:off use:REReds.var_inv unfold:R. Qed.
+
   Lemma univ_inj n i j :
     @R n (PUniv i) (PUniv j)  -> i = j.
   Proof.
     sauto lq:on rew:off use:REReds.univ_inv.
   Qed.
 
+  Lemma hne_app_inj n (a0 b0 a1 b1 : PTm n) :
+    R (PApp a0 b0) (PApp a1 b1) ->
+    ishne a0 ->
+    ishne a1 ->
+    R a0 a1 /\ R b0 b1.
+  Proof.
+    hauto lq:on use:REReds.hne_app_inv.
+  Qed.
+
+  Lemma hne_proj_inj n p0 p1 (a0 a1 : PTm n) :
+    R (PProj p0 a0) (PProj p1 a1) ->
+    ishne a0 ->
+    ishne a1 ->
+    p0 = p1 /\ R a0 a1.
+  Proof.
+    sauto lq:on use:REReds.hne_proj_inv.
+  Qed.
+
   Lemma FromRRed0 n (a b : PTm n) :
     RRed.R a b -> R a b.
   Proof.
@@ -2224,6 +2403,14 @@ Module DJoin.
     hauto lq:on rew:off ctrs:rtc unfold:R use:REReds.substing.
   Qed.
 
+  Lemma renaming n m (a b : PTm n) (ρ : fin n -> fin m) :
+    R a b -> R (ren_PTm ρ a) (ren_PTm ρ b).
+  Proof. substify. apply substing. Qed.
+
+  Lemma weakening n (a b : PTm n)  :
+    R a b -> R (ren_PTm shift a) (ren_PTm shift b).
+  Proof. apply renaming. Qed.
+
   Lemma cong n m (a : PTm (S n)) c d (ρ : fin n -> PTm m) :
     R c d -> R (subst_PTm (scons c ρ) a) (subst_PTm (scons d ρ) a).
   Proof.
@@ -2232,6 +2419,116 @@ Module DJoin.
     hauto q:on ctrs:rtc inv:option use:REReds.cong.
   Qed.
 
+  Lemma pair_inj n (a0 a1 b0 b1 : PTm n) :
+    SN (PPair a0 b0) ->
+    SN (PPair a1 b1) ->
+    R (PPair a0 b0) (PPair a1 b1) ->
+    R a0 a1 /\ R b0 b1.
+  Proof.
+    move => sn0 sn1.
+    have [? [? [? ?]]] : SN a0 /\ SN b0 /\ SN a1 /\ SN b1 by sfirstorder use:SN_NoForbid.P_PairInv.
+    have ? : SN (PProj PL (PPair a0 b0)) by hauto lq:on db:sn.
+    have ? : SN (PProj PR (PPair a0 b0)) by hauto lq:on db:sn.
+    have ? : SN (PProj PL (PPair a1 b1)) by hauto lq:on db:sn.
+    have ? : SN (PProj PR (PPair a1 b1)) by hauto lq:on db:sn.
+    have h0L : RRed.R (PProj PL (PPair a0 b0)) a0 by eauto with red.
+    have h0R : RRed.R (PProj PR (PPair a0 b0)) b0 by eauto with red.
+    have h1L : RRed.R (PProj PL (PPair a1 b1)) a1 by eauto with red.
+    have h1R : RRed.R (PProj PR (PPair a1 b1)) b1 by eauto with red.
+    move => h2.
+    move /ProjCong in h2.
+    have h2L := h2 PL.
+    have {h2}h2R := h2 PR.
+    move /FromRRed1 in h0L.
+    move /FromRRed0 in h1L.
+    move /FromRRed1 in h0R.
+    move /FromRRed0 in h1R.
+    split; eauto using transitive.
+  Qed.
+
+  Lemma ejoin_pair_inj n (a0 a1 b0 b1 : PTm n) :
+    nf a0 -> nf b0 -> nf a1 -> nf b1 ->
+    EJoin.R (PPair a0 b0) (PPair a1 b1) ->
+    EJoin.R a0 a1 /\ EJoin.R b0 b1.
+  Proof.
+    move => h0 h1 h2 h3 /FromEJoin.
+    have [? ?] : SN (PPair a0 b0) /\ SN (PPair a1 b1) by sauto lqb:on rew:off use:ne_nf_embed.
+    move => ?.
+    have : R a0 a1 /\ R b0 b1 by hauto l:on use:pair_inj.
+    hauto l:on use:ToEJoin.
+  Qed.
+
+  Lemma abs_inj n (a0 a1 : PTm (S n)) :
+    SN a0 -> SN a1 ->
+    R (PAbs a0) (PAbs a1) ->
+    R a0 a1.
+  Proof.
+    move => sn0 sn1.
+    move /weakening => /=.
+    move /AppCong. move /(_ (VarPTm var_zero) (VarPTm var_zero)).
+    move => /(_ ltac:(sfirstorder use:refl)).
+    move => h.
+    have /FromRRed1 h0 : RRed.R (PApp (PAbs (ren_PTm (upRen_PTm_PTm shift) a0)) (VarPTm var_zero)) a0 by apply RRed.AppAbs'; asimpl.
+    have /FromRRed0 h1 : RRed.R (PApp (PAbs (ren_PTm (upRen_PTm_PTm shift) a1)) (VarPTm var_zero)) a1 by apply RRed.AppAbs'; asimpl.
+    have sn0' := sn0.
+    have sn1' := sn1.
+    eapply sn_renaming with (ξ := (upRen_PTm_PTm shift)) in sn0.
+    eapply sn_renaming with (ξ := (upRen_PTm_PTm shift)) in sn1.
+    apply : transitive; try apply h0.
+    apply : N_Exp. apply N_β. sauto.
+    by asimpl.
+    apply : transitive; try apply h1.
+    apply : N_Exp. apply N_β. sauto.
+    by asimpl.
+    eauto.
+  Qed.
+
+  Lemma ejoin_abs_inj n (a0 a1 : PTm (S n)) :
+    nf a0 -> nf a1 ->
+    EJoin.R (PAbs a0) (PAbs a1) ->
+    EJoin.R a0 a1.
+  Proof.
+    move => h0 h1.
+    have [? [? [? ?]]] : SN a0 /\ SN a1 /\ SN (PAbs a0) /\ SN (PAbs a1) by sauto lqb:on rew:off use:ne_nf_embed.
+    move /FromEJoin.
+    move /abs_inj.
+    hauto l:on use:ToEJoin.
+  Qed.
+
+  Lemma standardization n (a b : PTm n) :
+    SN a -> SN b -> R a b ->
+    exists va vb, rtc RRed.R a va /\ rtc RRed.R b vb /\ nf va /\ nf vb /\ EJoin.R va vb.
+  Proof.
+    move => h0 h1 [ab [hv0 hv1]].
+    have hv : SN ab by sfirstorder use:REReds.sn_preservation.
+    have : exists v, rtc RRed.R ab v  /\ nf v by hauto q:on use:LoReds.FromSN, LoReds.ToRReds.
+    move => [v [hv2 hv3]].
+    have : rtc RERed.R a v by hauto q:on use:@relations.rtc_transitive, REReds.FromRReds.
+    have : rtc RERed.R b v by hauto q:on use:@relations.rtc_transitive, REReds.FromRReds.
+    move : h0 h1 hv3. clear.
+    move => h0 h1 hv hbv hav.
+    move : rered_standardization (h0) hav. repeat move/[apply].
+    move => [a1 [ha0 ha1]].
+    move : rered_standardization (h1) hbv. repeat move/[apply].
+    move => [b1 [hb0 hb1]].
+    have [*] : nf a1 /\ nf b1 by sfirstorder use:NeEPars.R_nonelim_nf.
+    hauto q:on use:NeEPars.ToEReds unfold:EJoin.R.
+  Qed.
+
+  Lemma standardization_lo n (a b : PTm n) :
+    SN a -> SN b -> R a b ->
+    exists va vb, rtc LoRed.R a va /\ rtc LoRed.R b vb /\ nf va /\ nf vb /\ EJoin.R va vb.
+  Proof.
+    move => /[dup] sna + /[dup] snb.
+    move : standardization; repeat move/[apply].
+    move => [va][vb][hva][hvb][nfva][nfvb]hj.
+    move /LoReds.FromSN : sna => [va' [hva' hva'0]].
+    move /LoReds.FromSN : snb => [vb' [hvb' hvb'0]].
+    exists va', vb'.
+    repeat split => //=.
+    have : va = va' /\ vb = vb' by sfirstorder use:red_uniquenf, LoReds.ToRReds.
+    case; congruence.
+  Qed.
 End DJoin.
 
 
@@ -2385,6 +2682,17 @@ Module Sub.
     qauto l:on inv:SNe.
   Qed.
 
+  Lemma hne_bind_noconf n (a b : PTm n) :
+    R a b -> ishne a -> isbind b -> False.
+  Proof.
+    rewrite /R.
+    move => [c[d] [? []]] h0 h1 h2 h3.
+    have : ishne c by eauto using REReds.hne_preservation.
+    have : isbind d by eauto using REReds.bind_preservation.
+    move : h1. clear. inversion 1; subst => //=.
+    clear. case : d => //=.
+  Qed.
+
   Lemma bind_sne_noconf n (a b : PTm n) :
     R a b -> SNe b -> isbind a -> False.
   Proof.

theories/soundness.v

@@ -10,3 +10,6 @@ Theorem fundamental_theorem :
   apply wt_mutual; eauto with sem; [hauto l:on use:SE_Pair].
   Unshelve. all : exact 0.
 Qed.
+
+Lemma synsub_to_usub : forall n Γ (a b : PTm n), Γ ⊢ a ≲ b -> SN a /\ SN b /\ Sub.R a b.
+Proof. hauto lq:on rew:off use:fundamental_theorem, SemLEq_SN_Sub. Qed.