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

More no forbid

Browse source
This commit is contained in:
Yiyun Liu 2025-01-29 22:14:01 -05:00
parent 99b5e87ea3
commit a47d69f427
1 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
theories/fp_red.v
View file

@ -426,6 +426,12 @@ Module RPar.
hauto q:on inv:option ctrs:R. hauto q:on inv:option ctrs:R.
Qed. Qed.
Lemma FromRRed n (a b : PTm n) :
RRed.R a b -> RPar.R a b.
Proof.
induction 1; qauto l:on use:RPar.refl ctrs:RPar.R.
Qed.
End RPar. End RPar.
Lemma red_sn_preservation n : Lemma red_sn_preservation n :
@ -788,6 +794,11 @@ Module SN_NoForbid : NoForbid.
Proof. sfirstorder use:ered_sn_preservation. Qed. Proof. sfirstorder use:ered_sn_preservation. Qed.
Lemma P_RRed : forall n (a b : PTm n), RRed.R a b -> P a -> P b. Lemma P_RRed : forall n (a b : PTm n), RRed.R a b -> P a -> P b.
Proof. hauto q:on use:red_sn_preservation, RPar.FromRRed. Qed.
Lemma P_AppPair : forall n (a b c : PTm n), ~ P (PApp (PPair a b) c).
Proof.
Lemma bool_dec (a : bool) : a \/ ~~ a. Lemma bool_dec (a : bool) : a \/ ~~ a.
Proof. hauto lq:on inv:bool. Qed. Proof. hauto lq:on inv:bool. Qed.