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

Add Abs_EPar'

Browse source
This commit is contained in:
Yiyun Liu 2024-12-23 23:44:57 -05:00
parent 86dab74384
commit 233f229b3f
1 changed files with 23 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
theories/fp_red.v
View file

@ -1,5 +1,5 @@
Require Import ssreflect. Require Import ssreflect.
From stdpp Require Import relations (rtc (..), rtc_once). From stdpp Require Import relations (rtc (..), rtc_once, rtc_r).
From Hammer Require Import Tactics. From Hammer Require Import Tactics.
Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax. Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.
@ -540,14 +540,21 @@ Lemma commutativity n (a b0 b1 : Tm n) :
hauto q:on ctrs:rtc. hauto q:on ctrs:rtc.
Qed. Qed.
Lemma EPar_Abs' n a (b : Tm n) : Lemma Abs_EPar' n a (b : Tm n) :
EPar.R (Abs a) b -> EPar.R (Abs a) b ->
exists d, EPar.R a d /\ EPar.R (Abs d) b. (exists d, EPar.R a d /\
rtc OExp.R (Abs d) b).
Proof. Proof.
move E : (Abs a) => u h. move E : (Abs a) => u h.
move : a E. move : a E.
elim : n u b /h => //=; elim : n u b /h => //=.
hauto lq:on rew:off ctrs:EPar.R use:EPar.refl. - move => n a0 a1 ha iha a ?. subst.
specialize iha with (1 := eq_refl).
hauto lq:on ctrs:OExp.R use:rtc_r.
- move => n a0 a1 ha iha a ?. subst.
specialize iha with (1 := eq_refl).
hauto lq:on ctrs:OExp.R use:rtc_r.
- hauto l:on ctrs:OExp.R.
Qed. Qed.
Lemma EPar_diamond n (c a1 b1 : Tm n) : Lemma EPar_diamond n (c a1 b1 : Tm n) :
@ -562,13 +569,20 @@ Proof.
- hauto lq:on rew:off ctrs:EPar.R. - hauto lq:on rew:off ctrs:EPar.R.
- hauto lq:on use:EPar.refl. - hauto lq:on use:EPar.refl.
- move => n a0 a1 ha iha a2 ha2. - move => n a0 a1 ha iha a2 ha2.
move /EPar_Abs' : (ha2). move /Abs_EPar' : (ha2).
move => [d [hd0 hd1]]. move => [d [hd0 hd1]].
move : iha (hd0); repeat move/[apply]. move : iha (hd0); repeat move/[apply].
move => [d2 [h0 h1]]. move => [d2 [h0 h1]].
exists (Abs d2). have : EPar.R (Abs d) (Abs d2) by eauto using EPar.AbsCong.
split. best. move : hd1.
best. move : OExp.commutativity0; repeat move/[apply].
move => [d1 [hd1 hd2]].
exists d1. split => //.
hauto lq:on ctrs:EPar.R use:OExp.merge.
- move => n a0 a1 b0 b1 ha iha hb ihb c hc.
admit.
- admit.
- best.