Move projection axioms to the subtyping relation

theories/common.v

@@ -0,0 +1,3 @@
+Require Import Autosubst2.fintype Autosubst2.syntax.
+Definition renaming_ok {n m} (Γ : fin n -> PTm n) (Δ : fin m -> PTm m) (ξ : fin m -> fin n) :=
+  forall (i : fin m), ren_PTm ξ (Δ i) = Γ (ξ i).

theories/logrel.v

@@ -1,5 +1,5 @@
 Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.
-Require Import fp_red.
+Require Import common fp_red.
 From Hammer Require Import Tactics.
 From Equations Require Import Equations.
 Require Import ssreflect ssrbool.
@@ -488,9 +488,6 @@ Lemma ρ_ok_cons' n i (Γ : fin n -> PTm n) ρ a PA A  Δ :
   ρ_ok Δ (scons a ρ).
 Proof. move => ->. apply ρ_ok_cons. Qed.
 
-Definition renaming_ok {n m} (Γ : fin n -> PTm n) (Δ : fin m -> PTm m) (ξ : fin m -> fin n) :=
-  forall (i : fin m), ren_PTm ξ (Δ i) = Γ (ξ i).
-
 Lemma ρ_ok_renaming n m (Γ : fin n -> PTm n) ρ :
   forall (Δ : fin m -> PTm m) ξ,
     renaming_ok Γ Δ ξ ->

theories/structural.v

@@ -0,0 +1,49 @@
+Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax common typing.
+From Hammer Require Import Tactics.
+Require Import ssreflect.
+
+
+Lemma lem :
+  (forall n (Γ : fin n -> PTm n), ⊢ Γ -> True) /\
+  (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> )  /\
+  (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> ...).
+Proof. apply wt_mutual. ...
+
+
+Lemma wff_mutual :
+  (forall n (Γ : fin n -> PTm n), ⊢ Γ -> True) /\
+  (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> ⊢ Γ)  /\
+  (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> ⊢ Γ).
+Proof. apply wt_mutual; eauto. Qed.
+
+#[export]Hint Constructors Wt Wff Eq : wt.
+
+Lemma renaming_up n m (ξ : fin n -> fin m) Δ Γ A :
+  renaming_ok Δ Γ ξ ->
+  renaming_ok (funcomp (ren_PTm shift) (scons (ren_PTm ξ A) Δ)) (funcomp (ren_PTm shift) (scons A Γ)) (upRen_PTm_PTm ξ) .
+Proof.
+  move => h i.
+  destruct i as [i|].
+  asimpl. rewrite /renaming_ok in h.
+  rewrite /funcomp. rewrite -h.
+  by asimpl.
+  by asimpl.
+Qed.
+
+Lemma renaming :
+  (forall n (Γ : fin n -> PTm n), ⊢ Γ -> True) /\
+  (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> forall m Δ (ξ : fin n -> fin m), ⊢ Δ -> renaming_ok Δ Γ ξ ->
+     Δ ⊢ ren_PTm ξ a ∈ ren_PTm ξ A) /\
+  (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> forall m Δ (ξ : fin n -> fin m), ⊢ Δ -> renaming_ok Δ Γ ξ ->
+     Δ ⊢ ren_PTm ξ a ≡ ren_PTm ξ b ∈ ren_PTm ξ A).
+Proof.
+  apply wt_mutual => //=; eauto 3 with wt.
+  - move => n Γ i hΓ _ m Δ ξ hΔ hξ.
+    rewrite hξ.
+    by apply T_Var.
+  - hauto lq:on rew:off ctrs:Wt, Wff  use:renaming_up.
+  - move => n Γ a A B i hP ihP ha iha m Δ ξ hΔ hξ.
+    apply : T_Abs; eauto.
+    apply iha; last by apply renaming_up.
+    econstructor; eauto.
+    by apply renaming_up.

theories/typing.v

@@ -2,6 +2,7 @@ Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.
 
 Reserved Notation "Γ ⊢ a ∈ A" (at level 70).
 Reserved Notation "Γ ⊢ a ≡ b ∈ A" (at level 70).
+Reserved Notation "Γ ⊢ A ≲ B" (at level 70).
 Reserved Notation "⊢ Γ" (at level 70).
 Inductive Wt : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> Prop :=
 | T_Var n Γ (i : fin n) :
@@ -37,13 +38,13 @@ Inductive Wt : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> Prop :=
   Γ ⊢ a ∈ PBind PSig A B ->
   Γ ⊢ PProj PR a ∈ subst_PTm (scons (PProj PL a) VarPTm) B
 
-| T_Univ n Γ i j :
-  i < j ->
-  Γ ⊢ PUniv i : PTm n ∈ PUniv j
+| T_Univ n Γ i :
+  ⊢ Γ ->
+  Γ ⊢ PUniv i : PTm n ∈ PUniv (S i)
 
-| T_Conv n Γ (a : PTm n) A B i :
+| T_Conv n Γ (a : PTm n) A B :
   Γ ⊢ a ∈ A ->
-  Γ ⊢ A ≡ B ∈ PUniv i ->
+  Γ ⊢ A ≲ B ->
   Γ ⊢ a ∈ B
 
 with Eq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> PTm n -> Prop :=
@@ -92,20 +93,38 @@ with Eq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> PTm n -> Prop :=
   Γ ⊢ a ≡ b ∈ PBind PSig A B ->
   Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B
 
-| E_Conv n Γ (a b : PTm n) A B i :
+| E_Conv n Γ (a b : PTm n) A B :
   Γ ⊢ a ≡ b ∈ A ->
-  Γ ⊢ B ∈ PUniv i ->
-  Γ ⊢ A ≡ B ∈ PUniv i ->
+  Γ ⊢ A ≲ B ->
   Γ ⊢ a ≡ b ∈ B
 
-| E_Bind_Proj1 n Γ p (A0 A1 : PTm n) B0 B1 i :
-  Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i ->
-  Γ ⊢ A0 ≡ A1 ∈ PUniv i
+with LEq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> Prop :=
+| Su_Transitive  n Γ (A B C : PTm n) :
+  Γ ⊢ A ≲ B ->
+  Γ ⊢ B ≲ C ->
+  Γ ⊢ A ≲ C
 
-| E_Bind_Proj2 n Γ p (a0 a1 A0 A1 : PTm n) B0 B1 i :
-  Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i ->
+| Su_Univ n Γ i j :
+  i <= j ->
+  Γ ⊢ PUniv i : PTm n ≲ PUniv j
+
+| Su_Bind n Γ p (A0 A1 : PTm n) B0 B1 :
+  Γ ⊢ A1 ≲ A0 ->
+  funcomp (ren_PTm shift) (scons A0 Γ) ⊢ B0 ≲ B1 ->
+  Γ ⊢ PBind p A0 B0 ≲ PBind p A1 B1
+
+| Su_Eq n Γ (A : PTm n) B i  :
+  Γ ⊢ A ≡ B ∈ PUniv i ->
+  Γ ⊢ A ≲ B
+
+| Su_Bind_Proj1 n Γ p (A0 A1 : PTm n) B0 B1 :
+  Γ ⊢ PBind p A0 B0 ≲ PBind p A1 B1 ->
+  Γ ⊢ A1 ≲ A0
+
+| Su_Bind_Proj2 n Γ p (a0 a1 A0 A1 : PTm n) B0 B1 :
+  Γ ⊢ PBind p A0 B0 ≲ PBind p A1 B1 ->
   Γ ⊢ a0 ≡ a1 ∈ A0 ->
-  Γ ⊢ subst_PTm (scons a0 VarPTm) B0 ≡ subst_PTm (scons a1 VarPTm) B1 ∈ PUniv i
+  Γ ⊢ subst_PTm (scons a0 VarPTm) B0 ≲ subst_PTm (scons a1 VarPTm) B1
 
 with Wff : forall {n}, (fin n -> PTm n) -> Prop :=
 | Wff_Nil :
@@ -117,10 +136,17 @@ with Wff : forall {n}, (fin n -> PTm n) -> Prop :=
   ⊢ funcomp (ren_PTm shift) (scons A Γ)
 
 where
-"Γ ⊢ a ∈ A" := (Wt Γ a A) and "⊢ Γ" := (Wff Γ) and "Γ ⊢ a ≡ b ∈ A" := (Eq Γ a b A).
+"Γ ⊢ a ∈ A" := (Wt Γ a A) and "⊢ Γ" := (Wff Γ) and "Γ ⊢ a ≡ b ∈ A" := (Eq Γ a b A) and "Γ ⊢ A ≲ B" := (LEq Γ A B).
 
 Scheme wf_ind := Induction for Wff Sort Prop
   with wt_ind := Induction for Wt Sort Prop
-  with eq_ind := Induction for Eq Sort Prop.
+  with eq_ind := Induction for Eq Sort Prop
+  with le_ind := Induction for LEq Sort Prop.
 
-Combined Scheme wt_mutual from wf_ind, wt_ind, eq_ind.
+Combined Scheme wt_mutual from wf_ind, wt_ind, eq_ind, le_ind.
+
+(* Lemma lem : *)
+(*   (forall n (Γ : fin n -> PTm n), ⊢ Γ -> ...) /\ *)
+(*   (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> ...)  /\ *)
+(*   (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> ...). *)
+(* Proof. apply wt_mutual. ... *)