Add alternative direct commutativity proof
This commit is contained in:
Yiyun Liu
parent
593f50ebaa
commit
5dbde6d45f
1 changed files with 76 additions and 80 deletions
|
|
@ -358,88 +358,84 @@ Proof.
|
||||||
move => + h. move : b. induction h; hauto lq:on ctrs:rtc use:ηO_commute.
|
move => + h. move : b. induction h; hauto lq:on ctrs:rtc use:ηO_commute.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
(* Lemma βη_commute0 a b c : *)
|
Lemma oexp_appabs b b' b0 a0 a1 :
|
||||||
(* βPar.R a b -> *)
|
rtc OExp.R (Abs b) b0 ->
|
||||||
(* ηPar.R a c -> *)
|
βPar.R b b' ->
|
||||||
(* exists d, ηPar.R b d /\ βPar.R c d. *)
|
βPar.R a0 a1 ->
|
||||||
(* Proof. *)
|
βPar.R (App b0 a0) (subst_Tm (scons a1 VarTm) b').
|
||||||
(* move => h. move : c. *)
|
Proof.
|
||||||
(* elim :a b /h. *)
|
move E : (Abs b) => u hu.
|
||||||
(* - move => i c. move /IO_factorization. *)
|
move : b E b' a0 a1.
|
||||||
(* move => [b [ihb0 ihb1]]. *)
|
elim : u b0 /hu => //=.
|
||||||
(* elim /IPar.inv : ihb0 => //=_. *)
|
- move => ? b ? b' a0 a1 hb ha. subst.
|
||||||
(* move => ? [*]. subst. *)
|
by constructor.
|
||||||
(* exists c. split. apply : IO_merge'; eauto. constructor. *)
|
- move => c0 c1 c2 hc0 hc1 ih b ? b' a0 a1 hb ha. subst.
|
||||||
(* apply βPar.refl. *)
|
elim /OExp.inv : hc0 => //= _.
|
||||||
(* - move => b0 b1 a0 a1 hb ihb ha iha u /IO_factorization. *)
|
move => ? ? ?. subst.
|
||||||
(* move => [v [+ hv]]. *)
|
specialize ih with (1 := eq_refl).
|
||||||
(* elim /IPar.inv => //=_. *)
|
apply ih => //.
|
||||||
(* move => b2 b3 a2 a3 hb2 ha2 [*]. subst. *)
|
eapply βPar.AppAbs' with (b1 := ren_Tm (upRen_Tm_Tm shift) b') (a1 := VarTm var_zero). by asimpl; rewrite subst_id.
|
||||||
(* rename b3 into b2. rename a3 into a2. *)
|
by apply βPar.renaming.
|
||||||
(* move : hb2 => {}/ihb. move => [b12 [ihb0 ihb1]]. *)
|
constructor.
|
||||||
(* move : ha2 => {}/iha. move => [a12 [iha0 iha1]]. *)
|
Qed.
|
||||||
(* have h2 : βPar.R (App b2 a2) (App b12 a12) by constructor. *)
|
|
||||||
(* move : βO_commute0 hv h2. repeat move/[apply]. *)
|
|
||||||
(* move => [v][h0 h1]. *)
|
|
||||||
(* exists v. split => //. apply : IO_merge'; eauto; by constructor. *)
|
|
||||||
(* - move => a0 a1 ha iha u /IO_factorization. *)
|
|
||||||
(* move => [v][hb0]hb1. *)
|
|
||||||
(* elim /IPar.inv : hb0 => //=_. *)
|
|
||||||
(* move => ? a2 + [*]. subst. *)
|
|
||||||
(* move => {}/iha. move => [a12 [ih0 ih1]]. *)
|
|
||||||
(* have {ih1} : βPar.R (Abs a2) (Abs a12) by constructor. *)
|
|
||||||
(* move : βO_commute0 hb1. repeat move/[apply]. *)
|
|
||||||
(* move => [d [h0 h1]]. exists d. split => //. *)
|
|
||||||
(* apply : IO_merge'; eauto; by constructor. *)
|
|
||||||
(* - move => b0 b1 a0 a1 hb ihb ha iha u /IO_factorization. *)
|
|
||||||
(* move => [v][hv0]hv1. *)
|
|
||||||
(* elim /IPar.inv : hv0 => //=_. *)
|
|
||||||
(* move => ? b2 ? a2 hb2 ha2 [*]. subst. *)
|
|
||||||
(* move /IO_factorization : hb2 => [b [h0 h1]]. *)
|
|
||||||
(* elim /IPar.inv : h0 => //=_. *)
|
|
||||||
(* move => ? b' ha' [*]. subst. *)
|
|
||||||
(* move : ihb ha' => /[apply]. move => [b12 [ihb0 ihb1]]. *)
|
|
||||||
(* move : iha ha2 => /[apply]. move => [a12 [iha0 iha1]]. *)
|
|
||||||
|
|
||||||
|
|
||||||
(* - move => b0 b1 a0 a1 hb ihb ha iha u. *)
|
|
||||||
(* elim /ηexp.inv => //=_. *)
|
|
||||||
(* + move => b2 b3 a2 hb' [*]. subst. *)
|
|
||||||
(* move : ihb hb' => /[apply]. move=> [b2 [ihb0 ihb1]]. *)
|
|
||||||
(* clear iha. *)
|
|
||||||
(* exists (App b2 a1). *)
|
|
||||||
(* split. *)
|
|
||||||
(* sfirstorder use:ηexps.AppCong, rtc_refl. *)
|
|
||||||
(* hauto lq:on ctrs:βPar.R use:βPar.refl. *)
|
|
||||||
(* + move => b2 ? a2 + [*]. subst. *)
|
|
||||||
(* move => {}/iha {ihb} [a12 [ih0 ih1]]. *)
|
|
||||||
|
|
||||||
|
|
||||||
(* Lemma ηβ_commute0 a b c : *)
|
|
||||||
(* ηPar.R a b -> *)
|
|
||||||
(* βPar.R a c -> *)
|
|
||||||
(* exists d, βPar.R b d /\ ηPar.R c d. *)
|
|
||||||
(* Proof. *)
|
|
||||||
(* move => h. move : c. elim : a b /h. *)
|
|
||||||
(* - hauto lq:on ctrs:βPar.R, ηPar.R inv:βPar.R. *)
|
|
||||||
(* - move => b0 b1 a0 a1 hb ihb ha iha u. *)
|
|
||||||
(* elim /βPar.inv => //=_. *)
|
|
||||||
(* + hauto lq:on ctrs:βPar.R, ηPar.R inv:βPar.R. *)
|
|
||||||
(* + move => b3 b2 a3 a2 hb2 ha2 [*]. subst. *)
|
|
||||||
(* rename b3 into b0. *)
|
|
||||||
(* have {}/ihb : βPar.R (Abs b0) (Abs b2) by eauto using βPar.AbsCong. *)
|
|
||||||
(* move => [b12 [ihb0 ihb1]]. *)
|
|
||||||
|
|
||||||
|
|
||||||
(* rename b3 into b4. rename b2 into b3. rename b4 into b2. *)
|
|
||||||
(* move => b2 b3 a2 a3 hb2 ha2 [*]. subst. *)
|
|
||||||
(* rename b3 into b2. rename a3 into a2. *)
|
|
||||||
(* move : ihb hb2 => /[apply]. move => [b12 [ihb0 ihb1]]. *)
|
|
||||||
(* move : iha ha2 => /[apply]. move => [a12 [iha0 iha1]]. *)
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
(* Direct commutativity proof with parallel η *)
|
||||||
Lemma βη_commute0 a b c :
|
Lemma βη_commute0 a b c :
|
||||||
|
βPar.R a b ->
|
||||||
|
ηPar.R a c ->
|
||||||
|
exists d, ηPar.R b d /\ βPar.R c d.
|
||||||
|
Proof.
|
||||||
|
move => h. move : c.
|
||||||
|
elim :a b /h.
|
||||||
|
- move => i c. move /IO_factorization.
|
||||||
|
move => [b [ihb0 ihb1]].
|
||||||
|
elim /IPar.inv : ihb0 => //=_.
|
||||||
|
move => ? [*]. subst.
|
||||||
|
exists c. split. apply : IO_merge'; eauto. constructor.
|
||||||
|
apply βPar.refl.
|
||||||
|
- move => b0 b1 a0 a1 hb ihb ha iha u /IO_factorization.
|
||||||
|
move => [v [+ hv]].
|
||||||
|
elim /IPar.inv => //=_.
|
||||||
|
move => b2 b3 a2 a3 hb2 ha2 [*]. subst.
|
||||||
|
rename b3 into b2. rename a3 into a2.
|
||||||
|
move : hb2 => {}/ihb. move => [b12 [ihb0 ihb1]].
|
||||||
|
move : ha2 => {}/iha. move => [a12 [iha0 iha1]].
|
||||||
|
have h2 : βPar.R (App b2 a2) (App b12 a12) by constructor.
|
||||||
|
move : βO_commute0 hv h2. repeat move/[apply].
|
||||||
|
move => [v][h0 h1].
|
||||||
|
exists v. split => //. apply : IO_merge'; eauto; by constructor.
|
||||||
|
- move => a0 a1 ha iha u /IO_factorization.
|
||||||
|
move => [v][hb0]hb1.
|
||||||
|
elim /IPar.inv : hb0 => //=_.
|
||||||
|
move => ? a2 + [*]. subst.
|
||||||
|
move => {}/iha. move => [a12 [ih0 ih1]].
|
||||||
|
have {ih1} : βPar.R (Abs a2) (Abs a12) by constructor.
|
||||||
|
move : βO_commute0 hb1. repeat move/[apply].
|
||||||
|
move => [d [h0 h1]]. exists d. split => //.
|
||||||
|
apply : IO_merge'; eauto; by constructor.
|
||||||
|
- move => b0 b1 a0 a1 hb ihb ha iha u /IO_factorization.
|
||||||
|
move => [v][hv0]hv1.
|
||||||
|
elim /IPar.inv : hv0 => //=_.
|
||||||
|
move => ? b2 ? a2 hb2 ha2 [*]. subst.
|
||||||
|
move /IO_factorization : hb2 => [b [h0 h1]].
|
||||||
|
elim /IPar.inv : h0 => //=_.
|
||||||
|
move => ? b' ha' [*]. subst.
|
||||||
|
move : ihb (ha') => /[apply]. move => [b12 [ihb0 ihb1]].
|
||||||
|
move : iha (ha2) => /[apply]. move => [a12 [iha0 iha1]].
|
||||||
|
have : βPar.R (App b2 a2) (subst_Tm (scons a12 VarTm) b12)
|
||||||
|
by eauto using oexp_appabs.
|
||||||
|
move : βO_commute0 hv1. repeat move/[apply].
|
||||||
|
move => [v][hv0]hv1.
|
||||||
|
exists v. split => //.
|
||||||
|
apply : IO_merge'; eauto.
|
||||||
|
apply ηPar.morphing2 => //.
|
||||||
|
apply ηPar.morphing2_ext => //.
|
||||||
|
move => *. constructor.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
(* Indirect but perhaps nicer proof with an extra
|
||||||
|
definition of full non-paralell η expansion *)
|
||||||
|
Lemma βη_commute0' a b c :
|
||||||
βPar.R a b ->
|
βPar.R a b ->
|
||||||
ηexp.R a c ->
|
ηexp.R a c ->
|
||||||
exists d, rtc ηexp.R b d /\ βPar.R c d.
|
exists d, rtc ηexp.R b d /\ βPar.R c d.
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue