yiyunliu/pair-eta
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Start refactoring to unscoped syntax

Browse source
This commit is contained in:
Yiyun Liu 2025-04-01 23:21:39 -04:00
parent 398a18d770
commit 9c17ec5cac
6 changed files with 994 additions and 1343 deletions
Download patch file Download diff file Expand all files Collapse all files

84
theories/fp_red.v
View file

@ -7,7 +7,7 @@ Require Import Arith.Wf_nat.
Require Import Psatz.
From stdpp Require Import relations (rtc (..), rtc_once, rtc_r).
From Hammer Require Import Tactics.
Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.
Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax.
Ltac2 spec_refl () :=
List.iter
@ -22,7 +22,7 @@ Ltac spec_refl := ltac2:(spec_refl ()).
(* Trying my best to not write C style module_funcname *)
Module Par.
Inductive R {n} : PTm n -> PTm n -> Prop :=
Inductive R : PTm -> PTm -> Prop :=
(***************** Beta ***********************)
| AppAbs a0 a1 b0 b1 :
R a0 a1 ->
@ -72,35 +72,35 @@ Module Par.
| Bot :
R PBot PBot.
Lemma refl n (a : PTm n) : R a a.
elim : n /a; hauto ctrs:R.
Lemma refl (a : PTm) : R a a.
elim : a; hauto ctrs:R.
Qed.
Lemma AppAbs' n a0 a1 (b0 b1 t : PTm n) :
Lemma AppAbs' a0 a1 (b0 b1 t : PTm) :
t = subst_PTm (scons b1 VarPTm) a1 ->
R a0 a1 ->
R b0 b1 ->
R (PApp (PAbs a0) b0) t.
Proof. move => ->. apply AppAbs. Qed.
Lemma ProjPair' n p (a0 a1 b0 b1 : PTm n) t :
Lemma ProjPair' p (a0 a1 b0 b1 : PTm) t :
t = (if p is PL then a1 else b1) ->
R a0 a1 ->
R b0 b1 ->
R (PProj p (PPair a0 b0)) t.
Proof. move => > ->. apply ProjPair. Qed.
Lemma AppEta' n (a0 a1 b : PTm n) :
Lemma AppEta' (a0 a1 b : PTm) :
b = (PAbs (PApp (ren_PTm shift a1) (VarPTm var_zero))) ->
R a0 a1 ->
R a0 b.
Proof. move => ->; apply AppEta. Qed.
Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
Lemma renaming (a b : PTm) (ξ : nat -> nat) :
R a b -> R (ren_PTm ξ a) (ren_PTm ξ b).
Proof.
move => h. move : m ξ.
elim : n a b /h.
move => h. move : ξ.
elim : a b /h.
move => *; apply : AppAbs'; eauto; by asimpl.
all : match goal with
| [ |- context[var_zero]] => move => *; apply : AppEta'; eauto; by asimpl
@ -109,23 +109,23 @@ Module Par.
Qed.
Lemma morphing n m (a b : PTm n) (ρ0 ρ1 : fin n -> PTm m) :
Lemma morphing (a b : PTm) (ρ0 ρ1 : nat -> PTm) :
(forall i, R (ρ0 i) (ρ1 i)) ->
R a b -> R (subst_PTm ρ0 a) (subst_PTm ρ1 b).
Proof.
move => + h. move : m ρ0 ρ1. elim : n a b/h.
- move => n a0 a1 b0 b1 ha iha hb ihb m ρ0 ρ1 hρ /=.
move => + h. move : ρ0 ρ1. elim : a b/h.
- move => a0 a1 b0 b1 ha iha hb ihb ρ0 ρ1 hρ /=.
eapply AppAbs' with (a1 := subst_PTm (up_PTm_PTm ρ1) a1); eauto.
by asimpl.
hauto l:on use:renaming inv:option.
hauto l:on use:renaming inv:nat.
- hauto lq:on rew:off ctrs:R.
- hauto l:on inv:option use:renaming ctrs:R.
- hauto l:on inv:nat use:renaming ctrs:R.
- hauto lq:on use:ProjPair'.
- move => n a0 a1 ha iha m ρ0 ρ1 hρ /=.
- move => a0 a1 ha iha ρ0 ρ1 hρ /=.
apply : AppEta'; eauto. by asimpl.
- hauto lq:on ctrs:R.
- sfirstorder.
- hauto l:on inv:option ctrs:R use:renaming.
- hauto l:on inv:nat ctrs:R use:renaming.
- hauto q:on ctrs:R.
- qauto l:on ctrs:R.
- qauto l:on ctrs:R.
@ -134,16 +134,16 @@ Module Par.
- qauto l:on ctrs:R.
Qed.
Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
Lemma substing (a b : PTm) (ρ : nat -> PTm) :
R a b -> R (subst_PTm ρ a) (subst_PTm ρ b).
Proof. hauto l:on use:morphing, refl. Qed.
Lemma antirenaming n m (a : PTm n) (b : PTm m) (ξ : fin n -> fin m) :
Lemma antirenaming (a : PTm) (b : PTm) (ξ : nat -> nat) :
R (ren_PTm ξ a) b -> exists b0, R a b0 /\ ren_PTm ξ b0 = b.
Proof.
move E : (ren_PTm ξ a) => u h.
move : n ξ a E. elim : m u b/h.
- move => n a0 a1 b0 b1 ha iha hb ihb m ξ []//=.
move : ξ a E. elim : u b/h.
- move => a0 a1 b0 b1 ha iha hb ihb ξ []//=.
move => c c0 [+ ?]. subst.
case : c => //=.
move => c [?]. subst.
@ -153,7 +153,7 @@ Module Par.
eexists. split.
apply AppAbs; eauto.
by asimpl.
- move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ξ []//=.
- move => a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc ξ []//=.
move => []//= t t0 t1 [*]. subst.
spec_refl.
move : iha => [? [*]].
@ -162,43 +162,43 @@ Module Par.
eexists. split.
apply AppPair; hauto. subst.
by asimpl.
- move => n p a0 a1 ha iha m ξ []//= p0 []//= t [*]. subst.
- move => p a0 a1 ha iha ξ []//= p0 []//= t [*]. subst.
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 ξ []//= p0 []//= t t0[*].
- move => p a0 a1 b0 b1 ha iha hb ihb ξ []//= p0 []//= t t0[*].
subst. spec_refl.
move : iha => [b0 [? ?]].
move : ihb => [c0 [? ?]]. subst.
eexists. split. by eauto using ProjPair.
hauto q:on.
- move => n a0 a1 ha iha m ξ a ?. subst.
- move => a0 a1 ha iha ξ a ?. subst.
spec_refl. move : iha => [a0 [? ?]]. subst.
eexists. split. apply AppEta; eauto.
by asimpl.
- move => n a0 a1 ha iha m ξ a ?. subst.
- move => a0 a1 ha iha ξ a ?. subst.
spec_refl. move : iha => [b0 [? ?]]. subst.
eexists. split. apply PairEta; eauto.
by asimpl.
- move => n i m ξ []//=.
- move => i ξ []//=.
hauto l:on.
- move => n a0 a1 ha iha m ξ []//= t [*]. subst.
- move => a0 a1 ha iha ξ []//= t [*]. subst.
spec_refl.
move :iha => [b0 [? ?]]. subst.
eexists. split. by apply AbsCong; eauto.
done.
- move => n a0 a1 b0 b1 ha iha hb ihb m ξ []//= t t0 [*]. subst.
- move => a0 a1 b0 b1 ha iha hb ihb ξ []//= t t0 [*]. subst.
spec_refl.
move : iha => [b0 [? ?]]. subst.
move : ihb => [c0 [? ?]]. subst.
eexists. split. by apply AppCong; eauto.
done.
- move => n a0 a1 b0 b1 ha iha hb ihb m ξ []//= t t0[*]. subst.
- move => a0 a1 b0 b1 ha iha hb ihb ξ []//= t t0[*]. subst.
spec_refl.
move : iha => [b0 [? ?]]. subst.
move : ihb => [c0 [? ?]]. subst.
eexists. split=>/=. by apply PairCong; eauto.
done.
- move => n p a0 a1 ha iha m ξ []//= p0 t [*]. subst.
- move => p a0 a1 ha iha ξ []//= p0 t [*]. subst.
spec_refl.
move : iha => [b0 [? ?]]. subst.
eexists. split. by apply ProjCong; eauto.
@ -359,7 +359,7 @@ Module RPar.
R a b ->
(forall i, R (ρ0 i) (ρ1 i)) ->
(forall i, R ((scons a ρ0) i) ((scons b ρ1) i)).
Proof. hauto q:on inv:option. Qed.
Proof. hauto q:on inv:nat. Qed.
Lemma morphing_up n m (ρ0 ρ1 : fin n -> PTm m) :
(forall i, R (ρ0 i) (ρ1 i)) ->
@ -399,7 +399,7 @@ Module RPar.
R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons d VarPTm) b).
Proof.
move => h0 h1. apply morphing => //=.
qauto l:on ctrs:R inv:option.
qauto l:on ctrs:R inv:nat.
Qed.
Lemma var_or_const_imp {n} (a b : PTm n) :
@ -595,7 +595,7 @@ Module RPar'.
R a b ->
(forall i, R (ρ0 i) (ρ1 i)) ->
(forall i, R ((scons a ρ0) i) ((scons b ρ1) i)).
Proof. hauto q:on inv:option. Qed.
Proof. hauto q:on inv:nat. Qed.
Lemma morphing_up n m (ρ0 ρ1 : fin n -> PTm m) :
(forall i, R (ρ0 i) (ρ1 i)) ->
@ -633,7 +633,7 @@ Module RPar'.
R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons d VarPTm) b).
Proof.
move => h0 h1. apply morphing => //=.
qauto l:on ctrs:R inv:option.
qauto l:on ctrs:R inv:nat.
Qed.
Lemma var_or_const_imp {n} (a b : PTm n) :
@ -786,7 +786,7 @@ Module ERed.
move => h. move : m ρ. elim : n a b / h => n.
move => a m ρ /=.
apply : AppEta'; eauto. by asimpl.
all : hauto ctrs:R inv:option use:renaming.
all : hauto ctrs:R inv:nat use:renaming.
Qed.
End ERed.
@ -892,11 +892,11 @@ Module EPar.
apply : AppEta'; eauto. by asimpl.
- hauto lq:on ctrs:R.
- hauto lq:on ctrs:R.
- hauto l:on ctrs:R use:renaming inv:option.
- hauto l:on ctrs:R use:renaming inv:nat.
- hauto q:on ctrs:R.
- hauto q:on ctrs:R.
- hauto q:on ctrs:R.
- hauto l:on ctrs:R use:renaming inv:option.
- hauto l:on ctrs:R use:renaming inv:nat.
- hauto lq:on ctrs:R.
- hauto lq:on ctrs:R.
Qed.
@ -907,7 +907,7 @@ Module EPar.
R (subst_PTm (scons b0 VarPTm) a0) (subst_PTm (scons b1 VarPTm) a1).
Proof.
move => h0 h1. apply morphing => //.
hauto lq:on ctrs:R inv:option.
hauto lq:on ctrs:R inv:nat.
Qed.
End EPar.
@ -1018,7 +1018,7 @@ Module RPars.
Lemma substing n (a b : PTm (S n)) c :
rtc RPar.R a b ->
rtc RPar.R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons c VarPTm) b).
Proof. hauto lq:on use:morphing inv:option. Qed.
Proof. hauto lq:on use:morphing inv:nat. Qed.
Lemma antirenaming n m (a : PTm n) (b : PTm m) (ρ : fin n -> PTm m) :
(forall i, var_or_const (ρ i)) ->
@ -1099,7 +1099,7 @@ Module RPars'.
Lemma substing n (a b : PTm (S n)) c :
rtc RPar'.R a b ->
rtc RPar'.R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons c VarPTm) b).
Proof. hauto lq:on use:morphing inv:option. Qed.
Proof. hauto lq:on use:morphing inv:nat. Qed.
Lemma antirenaming n m (a : PTm n) (b : PTm m) (ρ : fin n -> PTm m) :
(forall i, var_or_const (ρ i)) ->
@ -2328,7 +2328,7 @@ Proof.
have : wn (subst_PTm (scons (PBot) VarPTm) a3) by sfirstorder.
move => h. apply wn_abs.
move : h. apply wn_antirenaming.
hauto lq:on rew:off inv:option.
hauto lq:on rew:off inv:nat.
+ hauto q:on inv:RPar'.R ctrs:rtc b:on.
Qed.