From 233f229b3f0b76ccdff33e6516f09ad688df143e Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Mon, 23 Dec 2024 23:44:57 -0500 Subject: [PATCH] Add Abs_EPar' --- theories/fp_red.v | 32 +++++++++++++++++++++++--------- 1 file changed, 23 insertions(+), 9 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index 4d944e1..14db6d4 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -1,5 +1,5 @@ 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. 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. Qed. -Lemma EPar_Abs' n a (b : Tm n) : +Lemma Abs_EPar' n a (b : Tm n) : 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. move E : (Abs a) => u h. move : a E. - elim : n u b /h => //=; - hauto lq:on rew:off ctrs:EPar.R use:EPar.refl. + elim : n u b /h => //=. + - 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. 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 use:EPar.refl. - move => n a0 a1 ha iha a2 ha2. - move /EPar_Abs' : (ha2). + move /Abs_EPar' : (ha2). move => [d [hd0 hd1]]. move : iha (hd0); repeat move/[apply]. move => [d2 [h0 h1]]. - exists (Abs d2). - split. best. - best. + have : EPar.R (Abs d) (Abs d2) by eauto using EPar.AbsCong. + move : hd1. + 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.