Add admissible simple rules

theories/admissible.v

@@ -0,0 +1,50 @@
+Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax common typing structural.
+From Hammer Require Import Tactics.
+Require Import ssreflect.
+Require Import Psatz.
+Require Import Coq.Logic.FunctionalExtensionality.
+
+Derive Dependent Inversion wff_inv with (forall n (Γ : fin n -> PTm n), ⊢ Γ) Sort Prop.
+
+Lemma Wff_Cons_Inv n Γ (A : PTm n) :
+  ⊢ funcomp (ren_PTm shift) (scons A Γ) ->
+  ⊢ Γ /\ exists i, Γ ⊢ A ∈ PUniv i.
+Proof.
+  elim /wff_inv => //= _.
+  move => n0 Γ0 A0 i0 hΓ0 hA0 [? _]. subst.
+  Equality.simplify_dep_elim.
+  have h : forall i, (funcomp (ren_PTm shift) (scons A0 Γ0)) i = (funcomp (ren_PTm shift) (scons A Γ)) i by scongruence.
+  move /(_ var_zero) : (h).
+  rewrite /funcomp. asimpl.
+  move /ren_injective. move /(_ ltac:(hauto lq:on rew:off inv:option)).
+  move => ?. subst.
+  have : Γ0 = Γ. extensionality i.
+  move /(_ (Some i)) : h.
+  rewrite /funcomp. asimpl.
+  move /ren_injective. move /(_ ltac:(hauto lq:on rew:off inv:option)).
+  done.
+  move => ?. subst. sfirstorder.
+Qed.
+
+Lemma T_Abs n Γ (a : PTm (S n)) A B :
+  funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B ->
+  Γ ⊢ PAbs a ∈ PBind PPi A B.
+Proof.
+  move => ha.
+  have [i hB] : exists i, funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i by sfirstorder use:regularity.
+  have hΓ : ⊢ funcomp (ren_PTm shift) (scons A Γ) by sfirstorder use:wff_mutual.
+  move /Wff_Cons_Inv : hΓ => [hΓ][j]hA.
+  hauto lq:on rew:off use:T_Bind', typing.T_Abs.
+Qed.
+
+Lemma E_Bind n Γ i p (A0 A1 : PTm n) B0 B1 :
+  Γ ⊢ A0 ≡ A1 ∈ PUniv i ->
+  funcomp (ren_PTm shift) (scons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
+  Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i.
+Proof.
+  move => h0 h1.
+  have : Γ ⊢ A0 ∈ PUniv i by hauto l:on use:regularity.
+  have : ⊢ Γ by sfirstorder use:wff_mutual.
+  move : E_Bind h0 h1; repeat move/[apply].
+  firstorder.
+Qed.

theories/common.v

@@ -1,3 +1,47 @@
-Require Import Autosubst2.fintype Autosubst2.syntax.
+Require Import Autosubst2.fintype Autosubst2.syntax ssreflect.
+From Ltac2 Require Ltac2.
+Import Ltac2.Notations.
+Import Ltac2.Control.
+From Hammer Require Import Tactics.
+
 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).
+
+Local Ltac2 rec solve_anti_ren () :=
+  let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in
+  intro $x;
+  lazy_match! Constr.type (Control.hyp x) with
+  | fin _ -> _ _ => (ltac1:(case;hauto q:on depth:2))
+  | _ => solve_anti_ren ()
+  end.
+
+Local Ltac solve_anti_ren := ltac2:(Control.enter solve_anti_ren).
+
+Lemma up_injective n m (ξ : fin n -> fin m) :
+  (forall i j, ξ i = ξ j -> i = j) ->
+  forall i j, (upRen_PTm_PTm ξ)  i = (upRen_PTm_PTm ξ) j -> i = j.
+Proof.
+  sblast inv:option.
+Qed.
+
+Lemma ren_injective n m (a b : PTm n) (ξ : fin n -> fin m) :
+  (forall i j, ξ i = ξ j -> i = j) ->
+  ren_PTm ξ a = ren_PTm ξ b ->
+  a = b.
+Proof.
+  move : m ξ b.
+  elim : n / a => //; try solve_anti_ren.
+
+  move => n a iha m ξ []//=.
+  move => u hξ [h].
+  apply iha in h. by subst.
+  destruct i, j=>//=.
+  hauto l:on.
+
+  move => n p A ihA B ihB m ξ []//=.
+  move => b A0 B0  hξ [?]. subst.
+  move => ?. have ? : A0 = A by firstorder. subst.
+  move => ?. have : B = B0. apply : ihB; eauto.
+  sauto.
+  congruence.
+Qed.

theories/fp_red.v

@@ -8,7 +8,7 @@ Require Import Arith.Wf_nat (well_founded_lt_compat).
 Require Import Psatz.
 From stdpp Require Import relations (rtc (..), rtc_once, rtc_r, sn).
 From Hammer Require Import Tactics.
-Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.
+Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax common.
 Require Import Btauto.
 Require Import Cdcl.Itauto.
 
@@ -1408,35 +1408,6 @@ Module ERed.
   (*   destruct a. *)
   (*   exact (ξ f). *)
 
-  Lemma up_injective n m (ξ : fin n -> fin m) :
-    (forall i j, ξ i = ξ j -> i = j) ->
-    forall i j, (upRen_PTm_PTm ξ)  i = (upRen_PTm_PTm ξ) j -> i = j.
-  Proof.
-    sblast inv:option.
-  Qed.
-
-  Lemma ren_injective n m (a b : PTm n) (ξ : fin n -> fin m) :
-    (forall i j, ξ i = ξ j -> i = j) ->
-    ren_PTm ξ a = ren_PTm ξ b ->
-    a = b.
-  Proof.
-    move : m ξ b.
-    elim : n / a => //; try solve_anti_ren.
-
-    move => n a iha m ξ []//=.
-    move => u hξ [h].
-    apply iha in h. by subst.
-    destruct i, j=>//=.
-    hauto l:on.
-
-    move => n p A ihA B ihB m ξ []//=.
-    move => b A0 B0  hξ [?]. subst.
-    move => ?. have ? : A0 = A by firstorder. subst.
-    move => ?. have : B = B0. apply : ihB; eauto.
-    sauto.
-    congruence.
-  Qed.
-
   Lemma AppEta' n a u :
     u = (@PApp (S n) (ren_PTm shift a) (VarPTm var_zero)) ->
     R (PAbs u) a.