Make progress on wt_unique

2025-04-03 23:20:49 -04:00 · 2025-04-03 23:20:49 -04:00 · 5eb1f9df0b
commit 5eb1f9df0b
parent fbbce90304
6 changed files with 145 additions and 31 deletions
--- a/syntax.sig
+++ b/syntax.sig
@ -16,7 +16,7 @@ PPair : PTm -> PTm -> PTm
 PProj : PTag -> PTm -> PTm
 PConst : nat -> PTm

-Abs : (bind Tm in Tm) -> Tm
+Abs : Tm -> (bind Tm in Tm) -> Tm
 App : Tm -> Tm -> Tm
 Pair : Tm -> Tm -> Tm
 Proj : PTag -> Tm -> Tm
--- a/theories/Autosubst2/syntax.v
+++ b/theories/Autosubst2/syntax.v
@ -497,7 +497,7 @@ Qed.

 Inductive Tm : Type :=
  | VarTm : nat -> Tm
-  | Abs : Tm -> Tm
+  | Abs : Tm -> Tm -> Tm
  | App : Tm -> Tm -> Tm
  | Pair : Tm -> Tm -> Tm
  | Proj : PTag -> Tm -> Tm
@ -507,9 +507,11 @@ Inductive Tm : Type :=
  | Bool : Tm
  | If : Tm -> Tm -> Tm -> Tm.

-Lemma congr_Abs {s0 : Tm} {t0 : Tm} (H0 : s0 = t0) : Abs s0 = Abs t0.
+Lemma congr_Abs {s0 : Tm} {s1 : Tm} {t0 : Tm} {t1 : Tm} (H0 : s0 = t0)
+  (H1 : s1 = t1) : Abs s0 s1 = Abs t0 t1.
 Proof.
-exact (eq_trans eq_refl (ap (fun x => Abs x) H0)).
+exact (eq_trans (eq_trans eq_refl (ap (fun x => Abs x s1) H0))
+         (ap (fun x => Abs t0 x) H1)).
 Qed.

 Lemma congr_App {s0 : Tm} {s1 : Tm} {t0 : Tm} {t1 : Tm} (H0 : s0 = t0)
@ -574,7 +576,7 @@ Defined.
 Fixpoint ren_Tm (xi_Tm : nat -> nat) (s : Tm) {struct s} : Tm :=
  match s with
  | VarTm s0 => VarTm (xi_Tm s0)
-  | Abs s0 => Abs (ren_Tm (upRen_Tm_Tm xi_Tm) s0)
+  | Abs s0 s1 => Abs (ren_Tm xi_Tm s0) (ren_Tm (upRen_Tm_Tm xi_Tm) s1)
  | App s0 s1 => App (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1)
  | Pair s0 s1 => Pair (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1)
  | Proj s0 s1 => Proj s0 (ren_Tm xi_Tm s1)
@ -594,7 +596,7 @@ Defined.
 Fixpoint subst_Tm (sigma_Tm : nat -> Tm) (s : Tm) {struct s} : Tm :=
  match s with
  | VarTm s0 => sigma_Tm s0
-  | Abs s0 => Abs (subst_Tm (up_Tm_Tm sigma_Tm) s0)
+  | Abs s0 s1 => Abs (subst_Tm sigma_Tm s0) (subst_Tm (up_Tm_Tm sigma_Tm) s1)
  | App s0 s1 => App (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1)
  | Pair s0 s1 => Pair (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1)
  | Proj s0 s1 => Proj s0 (subst_Tm sigma_Tm s1)
@ -622,8 +624,9 @@ Fixpoint idSubst_Tm (sigma_Tm : nat -> Tm)
 subst_Tm sigma_Tm s = s :=
  match s with
  | VarTm s0 => Eq_Tm s0
-  | Abs s0 =>
-      congr_Abs (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s0)
+  | Abs s0 s1 =>
+      congr_Abs (idSubst_Tm sigma_Tm Eq_Tm s0)
+        (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s1)
  | App s0 s1 =>
      congr_App (idSubst_Tm sigma_Tm Eq_Tm s0) (idSubst_Tm sigma_Tm Eq_Tm s1)
  | Pair s0 s1 =>
@ -656,10 +659,10 @@ Fixpoint extRen_Tm (xi_Tm : nat -> nat) (zeta_Tm : nat -> nat)
 ren_Tm xi_Tm s = ren_Tm zeta_Tm s :=
  match s with
  | VarTm s0 => ap (VarTm) (Eq_Tm s0)
-  | Abs s0 =>
-      congr_Abs
+  | Abs s0 s1 =>
+      congr_Abs (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
        (extRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm)
-           (upExtRen_Tm_Tm _ _ Eq_Tm) s0)
+           (upExtRen_Tm_Tm _ _ Eq_Tm) s1)
  | App s0 s1 =>
      congr_App (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
        (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1)
@ -695,10 +698,10 @@ Fixpoint ext_Tm (sigma_Tm : nat -> Tm) (tau_Tm : nat -> Tm)
 subst_Tm sigma_Tm s = subst_Tm tau_Tm s :=
  match s with
  | VarTm s0 => Eq_Tm s0
-  | Abs s0 =>
-      congr_Abs
+  | Abs s0 s1 =>
+      congr_Abs (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
        (ext_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm) (upExt_Tm_Tm _ _ Eq_Tm)
-           s0)
+           s1)
  | App s0 s1 =>
      congr_App (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
        (ext_Tm sigma_Tm tau_Tm Eq_Tm s1)
@ -730,10 +733,10 @@ Fixpoint compRenRen_Tm (xi_Tm : nat -> nat) (zeta_Tm : nat -> nat)
 (s : Tm) {struct s} : ren_Tm zeta_Tm (ren_Tm xi_Tm s) = ren_Tm rho_Tm s :=
  match s with
  | VarTm s0 => ap (VarTm) (Eq_Tm s0)
-  | Abs s0 =>
-      congr_Abs
+  | Abs s0 s1 =>
+      congr_Abs (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
        (compRenRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm)
-           (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s0)
+           (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s1)
  | App s0 s1 =>
      congr_App (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
        (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1)
@ -772,10 +775,10 @@ Fixpoint compRenSubst_Tm (xi_Tm : nat -> nat) (tau_Tm : nat -> Tm)
 subst_Tm tau_Tm (ren_Tm xi_Tm s) = subst_Tm theta_Tm s :=
  match s with
  | VarTm s0 => Eq_Tm s0
-  | Abs s0 =>
-      congr_Abs
+  | Abs s0 s1 =>
+      congr_Abs (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
        (compRenSubst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm tau_Tm)
-           (up_Tm_Tm theta_Tm) (up_ren_subst_Tm_Tm _ _ _ Eq_Tm) s0)
+           (up_Tm_Tm theta_Tm) (up_ren_subst_Tm_Tm _ _ _ Eq_Tm) s1)
  | App s0 s1 =>
      congr_App (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
        (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1)
@ -828,10 +831,10 @@ Fixpoint compSubstRen_Tm (sigma_Tm : nat -> Tm) (zeta_Tm : nat -> nat)
 ren_Tm zeta_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
  match s with
  | VarTm s0 => Eq_Tm s0
-  | Abs s0 =>
-      congr_Abs
+  | Abs s0 s1 =>
+      congr_Abs (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
        (compSubstRen_Tm (up_Tm_Tm sigma_Tm) (upRen_Tm_Tm zeta_Tm)
-           (up_Tm_Tm theta_Tm) (up_subst_ren_Tm_Tm _ _ _ Eq_Tm) s0)
+           (up_Tm_Tm theta_Tm) (up_subst_ren_Tm_Tm _ _ _ Eq_Tm) s1)
  | App s0 s1 =>
      congr_App (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
        (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1)
@ -884,10 +887,10 @@ Fixpoint compSubstSubst_Tm (sigma_Tm : nat -> Tm) (tau_Tm : nat -> Tm)
 subst_Tm tau_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
  match s with
  | VarTm s0 => Eq_Tm s0
-  | Abs s0 =>
-      congr_Abs
+  | Abs s0 s1 =>
+      congr_Abs (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
        (compSubstSubst_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm)
-           (up_Tm_Tm theta_Tm) (up_subst_subst_Tm_Tm _ _ _ Eq_Tm) s0)
+           (up_Tm_Tm theta_Tm) (up_subst_subst_Tm_Tm _ _ _ Eq_Tm) s1)
  | App s0 s1 =>
      congr_App (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
        (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1)
@ -981,10 +984,10 @@ Fixpoint rinst_inst_Tm (xi_Tm : nat -> nat) (sigma_Tm : nat -> Tm)
   : ren_Tm xi_Tm s = subst_Tm sigma_Tm s :=
  match s with
  | VarTm s0 => Eq_Tm s0
-  | Abs s0 =>
-      congr_Abs
+  | Abs s0 s1 =>
+      congr_Abs (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
        (rinst_inst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm sigma_Tm)
-           (rinstInst_up_Tm_Tm _ _ Eq_Tm) s0)
+           (rinstInst_up_Tm_Tm _ _ Eq_Tm) s1)
  | App s0 s1 =>
      congr_App (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
        (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1)
--- a/theories/compile.v
+++ b/theories/compile.v
@ -10,7 +10,7 @@ Module Compile.
    match a with
    | TBind p A B => PPair (PPair (PConst (compileTag p)) (F A)) (PAbs (F B))
    | Univ i => PConst (3 + i)
-    | Abs a => PAbs (F a)
+    | Abs _ a => PAbs (F a)
    | App a b => PApp (F a) (F b)
    | VarTm i => VarPTm i
    | Pair a b => PPair (F a) (F b)
@ -75,6 +75,17 @@ Module Join.
    tauto.
  Qed.

+  Lemma BindCong p A0 A1 B0 B1 :
+    R A0 A1 ->
+    R B0 B1 ->
+    R (TBind p A0 B0) (TBind p A1 B1).
+  Proof.
+    move => h0 h1. rewrite /R /=.
+    apply join_pair_inj.
+    split. apply join_pair_inj. split. apply join_refl. done.
+    by apply Join.AbsCong.
+  Qed.
+
  Lemma UnivInj i j : R (Univ i : Tm) (Univ j) -> i = j.
  Proof. hauto l:on use:join_const_inj. Qed.

--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@ -2147,6 +2147,20 @@ Proof.
    apply join_symmetric. apply Join.FromPar. apply Par.AppEta. apply Par.refl.
 Qed.

+(* Lemma abs_inj a b : *)
+(*   join a b <-> join (PAbs a) (PAbs b). *)
+(* Proof. *)
+(*   split. *)
+
+(*   transitivity (join a (PApp (ren_PTm shift (PAbs b)) (VarPTm var_zero))); last by rewrite abs_eq. *)
+(*   have h : RPar.R (PApp (ren_PTm shift (PAbs b)) (VarPTm var_zero)) (subst_PTm (scons (VarPTm var_zero) VarPTm) (ren_PTm (upRen_PTm_PTm shift) b)). *)
+(*   apply RPar.AppAbs. rewrite -/ren_PTm. asimpl. substify. asimpl. apply RPar.refl. apply RPar.refl. *)
+(*   split. *)
+(*   move => h1. apply : join_transitive; eauto. *)
+(*   apply join_symmetric. *)
+(*   apply  *)
+
+
 Lemma pair_eq (a0 a1 b : PTm) :
  join (PPair a0 a1) b <-> join a0 (PProj PL b) /\ join a1 (PProj PR b).
 Proof.
--- a/theories/typing.v
+++ b/theories/typing.v
@ -39,7 +39,7 @@ Inductive Wt : list Tm -> Tm -> Tm -> Prop :=
 | T_Abs Γ a A B i :
  Γ ⊢ TBind TPi A B ∈ (Univ i) ->
  (cons A Γ) ⊢ a ∈ B ->
-  Γ ⊢ Abs a ∈ TBind TPi A B
+  Γ ⊢ Abs A a ∈ TBind TPi A B

 | T_App Γ b a A B :
  Γ ⊢ b ∈ TBind TPi A B ->
--- a/theories/typing_properties.v
+++ b/theories/typing_properties.v
@ -1,2 +1,88 @@
 Require Import Autosubst2.core Autosubst2.unscoped compile Autosubst2.syntax ssreflect typing.
 From Hammer Require Import Tactics.
+
+Lemma Bind_Inv Γ p A B U :
+  Γ ⊢ TBind p A B ∈ U ->
+  exists i, Γ ⊢ A ∈ Univ i /\ cons A Γ ⊢ B ∈ Univ i /\ Join.R (Univ i) U.
+Proof.
+  move E : (TBind p A B) => u hu.
+  move : p A B E.
+  elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
+Qed.
+
+Lemma Univ_Inv Γ i  U :
+  Γ ⊢ Univ i ∈ U ->
+  Γ ⊢ Univ i ∈ Univ (S i) /\ Join.R (Univ (S i)) U.
+Proof.
+  move E : (Univ i) => u hu.
+  move : i E.
+  elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
+Qed.
+
+Lemma App_Inv Γ b a U :
+  Γ ⊢ App b a ∈ U ->
+  exists A B, Γ ⊢ b ∈ TBind TPi A B /\ Γ ⊢ a ∈ A /\ Join.R (subst_Tm (scons a VarTm) B) U.
+Proof.
+  move E : (App b a) => u hu.
+  move : b a E.
+  elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
+Qed.
+
+Lemma Abs_Inv Γ A a U :
+  Γ ⊢ Abs A a ∈ U ->
+  exists B, cons A Γ ⊢ a ∈ B /\ Join.R (TBind TPi A B) U.
+Proof.
+  move E : (Abs A a) => u hu.
+  move : A a E.
+  elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
+Qed.
+
+Lemma Var_Inv Γ i U :
+  Γ ⊢ VarTm i ∈ U ->
+  exists A, lookup i Γ A /\ Join.R A U.
+Proof.
+  move E : (VarTm i) => u hu.
+  move : i E.
+  elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
+Qed.
+
+Lemma ctx_wff_mutual :
+  (forall Γ, ⊢ Γ -> True) /\
+  (forall Γ a A, Γ ⊢ a ∈ A -> ⊢ Γ).
+Proof. apply wt_mutual => //=. Qed.
+
+Lemma lookup_deter i Γ A A0 :
+  lookup i Γ A ->
+  lookup i Γ A0 -> A = A0.
+Proof.
+  move => h. move : A0. elim : i Γ A / h; hauto lq:on inv:lookup.
+Qed.
+
+Lemma wt_unique :
+  (forall Γ, ⊢ Γ -> True) /\
+  (forall Γ a A, Γ ⊢ a ∈ A -> forall B, Γ ⊢ a ∈ B -> Join.R A B).
+Proof.
+  apply wt_mutual => //=.
+  - move => i Γ A hΓ _ hl B.
+    move /Var_Inv.
+    move => [A0 [h0 h1]].
+    move : hl h0.
+    move : lookup_deter; repeat move/[apply]. move => ?. by subst.
+  - move => Γ i p A B hA ihA hB ihB U.
+    move /Bind_Inv => [j][ih0][ih1]ih2.
+    apply ihB in ih1.
+    move /Join.UnivInj in ih1. by subst.
+  - move => Γ a A B i hP ihP ha iha U.
+    move /Abs_Inv => [B0][ha']hJ.
+    move /iha in ha' => {iha}.
+    apply : Join.transitive; eauto.
+    apply Join.BindCong; eauto using Join.reflexive.
+  - move => Γ b a A B hb ihb ha iha U.
+    move /App_Inv. move => [A0][B0][hb'][ha']hU.
+    apply ihb in hb' => {ihb}.
+    move /Join.BindInj : hb'.
+    move => [_][hJ0]hJ1.
+    apply : Join.transitive; eauto.
+    by apply Join.substing.
+  - move => Γ a b A B i hS ihS ha iha hb ihb U.
+Admitted.