From d933920270e136e881d1f6f1c8fce3a4b79f5ab4 Mon Sep 17 00:00:00 2001 From: Gil Hur Date: Mon, 5 Oct 2020 07:26:23 +0900 Subject: [PATCH 1/3] Start the Indexed Coinduction. --- _CoqConfig | 1 + theories/Basics/GeneralWFO.v | 644 +++++++++++++ theories/Eq/Eq.v | 1675 +++++++++++++++++++++++----------- 3 files changed, 1775 insertions(+), 545 deletions(-) create mode 100644 theories/Basics/GeneralWFO.v diff --git a/_CoqConfig b/_CoqConfig index e73ea61c..e43caf2e 100644 --- a/_CoqConfig +++ b/_CoqConfig @@ -21,6 +21,7 @@ theories/Basics/CategoryKleisli.v theories/Basics/CategoryKleisliFacts.v theories/Basics/Function.v theories/Basics/FunctionFacts.v +theories/Basics/GeneralWFO.v theories/Core/ITreeDefinition.v theories/Core/KTree.v diff --git a/theories/Basics/GeneralWFO.v b/theories/Basics/GeneralWFO.v new file mode 100644 index 00000000..5ad9d79f --- /dev/null +++ b/theories/Basics/GeneralWFO.v @@ -0,0 +1,644 @@ +(** Well-founded orders. *) + +Require Import Arith Relations Max NPeano Program Wellfounded List Lia. +From Paco Require Import paco. +Import ListNotations. + +Set Implicit Arguments. +Global Set Bullet Behavior "Strict Subproofs". + +Ltac ginduction H := + move H at top; revert_until H; induction H. + +(** * Additions to the Relations library. *) + +Notation rtc := (clos_refl_trans _). (* reflexive transitive closure *) +Notation tc := (clos_trans _). (* transitive closure *) +Hint Immediate rt_step rt_refl t_step. + +Lemma tc_well_founded: forall A R + (WF: @well_founded A R), + well_founded (tc R). +Proof. clear. + red; intros; induction a using (well_founded_ind WF); econstructor; intros. + apply clos_trans_tn1_iff in H0; induction H0; eauto. + apply IHclos_trans_n1; specialize (H y0 H0); inversion H; eauto. +Qed. + +Lemma rtc_mon: forall X (R R': X -> X -> Prop) a b + (IN: rtc R a b) + (LE: R <2= R'), + rtc R' a b. +Proof. + intros; induction IN; [econstructor 1|econstructor 2|econstructor 3]; eauto. +Qed. + +Lemma tc_mon: forall X (R R': X -> X -> Prop) a b + (IN: tc R a b) + (LE: R <2= R'), + tc R' a b. +Proof. + intros; induction IN; [econstructor 1|econstructor 2]; eauto. +Qed. + +Lemma tc_rtc: forall X r (a b: X) + (TC: tc r a b), + rtc r a b. +Proof. + intros; induction TC; eauto using rt_trans. +Qed. + +Lemma rtc_tc: forall X r (a b: X) + (RTC: rtc r a b), + a = b \/ tc r a b. +Proof. + intros; induction RTC; eauto. + destruct IHRTC1, IHRTC2; subst; eauto. + right; econstructor 2; eauto. +Qed. + +Lemma tc_rtc_tc: forall X r (a b c: X) + (TC: tc r a b) + (RTC: rtc r b c), + tc r a c. +Proof. + intros; induction RTC; eauto using t_trans, t_step. +Qed. + +Lemma rtc_tc_tc: forall X r (a b c: X) + (RTC: rtc r a b) + (TC: tc r b c), + tc r a c. +Proof. + intros; induction RTC; eauto using t_trans, t_step. +Qed. + +Lemma tc_first: forall X r (a c: X) + (CT: tc r a c), + exists b, r a b /\ rtc r b c. +Proof. + intros. induction CT; eauto using rt_refl; clear IHCT2. + destruct IHCT1 as [? []]. + eauto using rt_step, tc_rtc, rtc_tc_tc. +Qed. + +Lemma tc_last: forall X r (a c: X) + (CT: tc r a c), + exists b, rtc r a b /\ r b c. +Proof. + intros; induction CT; eauto using rt_refl; clear IHCT1. + destruct IHCT2 as [? []]. + eauto using rt_step, tc_rtc, tc_rtc_tc. +Qed. + +(** * Definitions. *) + +(** ** + Wellfounded Order + *) + +Structure bwfo := + { bwfo_set :> Type; + bwfo_lt : bwfo_set -> bwfo_set -> Prop; + bwfo_le : bwfo_set -> bwfo_set -> Prop; + + bwfo_le_refl: forall i, bwfo_le i i; + bwfo_lt_le: forall i j, bwfo_lt i j -> bwfo_le i j; + bwfo_le_le_le: forall i j k, bwfo_le i j -> bwfo_le j k -> bwfo_le i k; + bwfo_lt_le_lt: forall i j k, bwfo_lt i j -> bwfo_le j k -> bwfo_lt i k; + bwfo_le_lt_lt: forall i j k, bwfo_le i j -> bwfo_lt j k -> bwfo_lt i k; + + bwfo_wf : well_founded bwfo_lt; +}. +Arguments bwfo_lt {_} _ _. +Arguments bwfo_le {_} _ _. + +(* ** + Symmetric Product of Algebraic Wellfounded Orders + *) + +Definition symprod_lt (a b : bwfo) (x y: a * b) := + (bwfo_lt (fst x) (fst y) /\ bwfo_le (snd x) (snd y)) \/ + (bwfo_le (fst x) (fst y) /\ bwfo_lt (snd x) (snd y)). + +Definition symprod_le (a b : bwfo) (x y: a * b) := + bwfo_le (fst x) (fst y) /\ bwfo_le (snd x) (snd y). + +Program Definition bwfo_symprod (a b : bwfo) : bwfo := + {| bwfo_lt := symprod_lt a b; + bwfo_le := symprod_le a b; + |}. +Next Obligation. split; simpl; eauto using bwfo_le_refl. Qed. +Next Obligation. + destruct H as [[]|[]]; split; simpl in *; eauto using bwfo_lt_le, bwfo_le_le_le. +Qed. +Next Obligation. + destruct H, H0; split; simpl in *; eauto using bwfo_le_le_le. +Qed. +Next Obligation. + destruct H, H, H0; [left|right]; split; simpl in *; eauto using bwfo_lt_le_lt, bwfo_le_le_le. +Qed. +Next Obligation. + destruct H, H0, H0; [left|right]; split; simpl in *; eauto using bwfo_le_lt_lt, bwfo_le_le_le. +Qed. +Next Obligation. + intros [u v]. + assert (WFu := bwfo_wf _ u). revert v. + induction WFu as [u _ HYPu]. + econstructor; intros [u' v'] LT'. + destruct LT', H; simpl in *. + - eapply HYPu in H; eauto. + - clear v H0. + assert (WFv' := bwfo_wf _ v'). revert u' H. + induction WFv' as [v' _ HYPv']. + econstructor; intros [u'' v''] LT''. + destruct LT'', H0; simpl in *. + + eapply HYPu; eauto using bwfo_lt_le_lt. + + eapply HYPv'; eauto using bwfo_le_le_le. +Qed. + +(* ** + Lexcographic Product of Algebraic Wellfounded Orders + *) + +Definition lexprod_lt (a b : bwfo) (x y: a * b) := + bwfo_lt (fst x) (fst y) \/ + (bwfo_le (fst x) (fst y) /\ bwfo_lt (snd x) (snd y)). + +Definition lexprod_le (a b : bwfo) (x y: a * b) := + bwfo_lt (fst x) (fst y) \/ + (bwfo_le (fst x) (fst y) /\ bwfo_le (snd x) (snd y)). + +Program Definition bwfo_lexprod (a b : bwfo) : bwfo := + {| bwfo_lt := lexprod_lt a b; + bwfo_le := lexprod_le a b; + |}. +Next Obligation. right. split; simpl; eauto using bwfo_le_refl. Qed. +Next Obligation. + destruct H as [|[]]; [left|right]; simpl in *; eauto using bwfo_lt_le. +Qed. +Next Obligation. + destruct H as [|[]], H0 as [|[]]; [..|right]; try left; simpl in *; eauto using bwfo_lt_le, bwfo_lt_le_lt, bwfo_le_lt_lt, bwfo_le_le_le. +Qed. +Next Obligation. + destruct H as [|[]], H0 as [|[]]; [..|right]; try left; simpl in *; eauto using bwfo_lt_le, bwfo_lt_le_lt, bwfo_le_lt_lt, bwfo_le_le_le. +Qed. +Next Obligation. + destruct H as [|[]], H0 as [|[]]; [..|right]; try left; simpl in *; eauto using bwfo_lt_le, bwfo_lt_le_lt, bwfo_le_lt_lt, bwfo_le_le_le. +Qed. +Next Obligation. + intros [u v]. + assert (WFu := bwfo_wf _ u). revert v. + induction WFu as [u _ HYPu]. + econstructor; intros [u' v'] LT'. + destruct LT' as [|[]]; simpl in *. + - eapply HYPu in H; eauto. + - clear v H0. + assert (WFv' := bwfo_wf _ v'). revert u' H. + induction WFv' as [v' _ HYPv']. + econstructor; intros [u'' v''] LT''. + destruct LT'' as [|[]]; simpl in *. + + eapply HYPu; eauto using bwfo_lt_le_lt. + + eapply HYPv'; eauto using bwfo_le_le_le. +Qed. + +(** ** + Non-trival Non-negative Well-founded Ordered Monoids + *) + +Structure awfo := +{ wfo_set :> Type; + + wfo_zero : wfo_set; + wfo_add : wfo_set -> wfo_set -> wfo_set; + + wfo_lt : wfo_set -> wfo_set -> Prop; + wfo_le : wfo_set -> wfo_set -> Prop; + +(* Monoid *) + + wfo_add_zero_l_le: forall i, wfo_le (wfo_add wfo_zero i) i; + wfo_add_zero_l_ge: forall i, wfo_le i (wfo_add wfo_zero i); + wfo_add_zero_r_le: forall i, wfo_le (wfo_add i wfo_zero) i; + wfo_add_zero_r_ge: forall i, wfo_le i (wfo_add i wfo_zero); + + wfo_add_assoc_le: forall i j k, wfo_le (wfo_add i (wfo_add j k)) (wfo_add (wfo_add i j) k); + wfo_add_assoc_ge: forall i j k, wfo_le (wfo_add (wfo_add i j) k) (wfo_add i (wfo_add j k)); + +(* Order *) + + wfo_le_refl: forall i, wfo_le i i; + wfo_lt_le: forall i j, wfo_lt i j -> wfo_le i j; + wfo_le_le_le: forall i j k, wfo_le i j -> wfo_le j k -> wfo_le i k; + wfo_lt_le_lt: forall i j k, wfo_lt i j -> wfo_le j k -> wfo_lt i k; + wfo_le_lt_lt: forall i j k, wfo_le i j -> wfo_lt j k -> wfo_lt i k; + + wfo_add_le_left: forall i i' j (LE: wfo_le i i'), wfo_le (wfo_add i j) (wfo_add i' j); + wfo_add_le_right: forall i j j' (LE: wfo_le j j'), wfo_le (wfo_add i j) (wfo_add i j'); + wfo_add_lt_left: forall i i' j (LT: wfo_lt i i'), wfo_lt (wfo_add i j) (wfo_add i' j); + wfo_add_lt_right: forall i j j' (LT: wfo_lt j j'), wfo_lt (wfo_add i j) (wfo_add i j'); + +(* Well-founded *) + wfo_wf : well_founded wfo_lt; + +(* Positive *) + wfo_non_negative: forall i, wfo_le wfo_zero i; + +(* Non-trivial *) + wfo_one : wfo_set; + wfo_non_trivial : wfo_lt wfo_zero wfo_one; +}. + +Arguments wfo_lt {_} _ _. +Arguments wfo_le {_} _ _. +Arguments wfo_zero {_}. +Arguments wfo_one {_}. +Arguments wfo_add {_} _ _. + +(* ** + General Wellfounded Order in NtNnWfPoMonoid + *) + +Definition gwf_set : Type := list (sigT bwfo_set). + +Definition gwfel (o: bwfo) (x: o) := + existT _ o x. + +Program Definition unit_wfo : bwfo := + {| bwfo_set := unit; + bwfo_lt _ _ := False; + bwfo_le _ _ := True; + |}. +Next Obligation. econstructor; intros. contradiction. Qed. + +Definition gwf_one : gwf_set := + [ gwfel unit_wfo tt ]. + +Inductive gwf_lex (b: bool) : gwf_set -> gwf_set -> Prop := +| gwf_lex_nil + (CHECK: is_true b) + : gwf_lex b [] [] +| gwf_lex_lt + o x y i j + (LT: bwfo_lt x y) + (LEN: length i = length j) + : gwf_lex b (gwfel o x :: i) (gwfel o y :: j) +| gwf_lex_step + o x y i j + (LE: bwfo_le x y) + (CMP: gwf_lex b i j) + : gwf_lex b (gwfel o x :: i) (gwfel o y :: j) +. +Hint Constructors gwf_lex. + +Variant gwf_cmp b : gwf_set -> gwf_set -> Prop := +| gwf_cmp_lt + o1 o2 + (LEN: length o1 < length o2) + : gwf_cmp b o1 o2 +| gwf_cmp_lex + i j + (CMP: gwf_lex b i j) + : gwf_cmp b i j +. +Hint Constructors gwf_cmp. + +Lemma gwf_lex_length b o1 o2 + (LT: gwf_lex b o1 o2) + : length o1 = length o2. +Proof. + intros. induction LT; simpl; nia. +Qed. + +Lemma gwf_cmp_length b o1 o2 + (CMP: gwf_cmp b o1 o2) + : length o1 <= length o2. +Proof. + destruct CMP. + - nia. + - erewrite gwf_lex_length; eauto. +Qed. + +Lemma gwf_lex_refl: forall i, gwf_lex true i i. +Proof. + induction i; eauto. + destruct a. eapply gwf_lex_step; eauto using bwfo_le_refl. +Qed. + +Lemma gwf_le_refl: forall i, gwf_cmp true i i. +Proof. + intros. apply gwf_cmp_lex. eauto using gwf_lex_refl. +Qed. + +Lemma gwf_lex_lt_le: forall i j, gwf_lex false i j -> gwf_lex true i j. +Proof. + intros. induction H; eauto. +Qed. + +Lemma gwf_lt_le: forall i j, gwf_cmp false i j -> gwf_cmp true i j. +Proof. + intros. destruct H; eauto using gwf_lex_lt_le. +Qed. + +Lemma gwf_lex_trans b1 b2 b3 i j k + (COND: is_true (b1 && b2) -> is_true b3) + (CMP1: gwf_lex b1 i j) + (CMP2: gwf_lex b2 j k) + : gwf_lex b3 i k. +Proof. + ginduction CMP2; intros. + - inversion CMP1; subst. destruct b1, b2, b3; eauto. + - dependent destruction CMP1. + + eapply gwf_lex_lt; eauto using bwfo_le_lt_lt, bwfo_lt_le. + nia. + + eapply gwf_lex_lt; eauto using bwfo_le_lt_lt. + apply gwf_lex_length in CMP1. nia. + - dependent destruction CMP1. + + eapply gwf_lex_lt; eauto using bwfo_lt_le_lt. + apply gwf_lex_length in CMP2. nia. + + eapply gwf_lex_step; eauto using bwfo_le_le_le. +Qed. + +Lemma gwf_cmp_trans b1 b2 b3 i j k + (CMP1: gwf_cmp b1 i j) + (CMP2: gwf_cmp b2 j k) + (COND: is_true (b1 && b2) -> is_true b3) + : gwf_cmp b3 i k. +Proof. + assert (LE1 := gwf_cmp_length CMP1). + assert (LE2 := gwf_cmp_length CMP2). + destruct CMP1, CMP2; eauto using gwf_lex_trans; apply gwf_cmp_lt; nia. +Qed. + +Lemma gwf_add_cmp_left b: forall i i' j (LE: gwf_cmp b i i'), gwf_cmp b (i ++ j) (i' ++ j). +Proof. + intros. inversion LE; subst. + - apply gwf_cmp_lt. rewrite !app_length. nia. + - apply gwf_cmp_lex. + induction CMP; simpl. + + destruct b; inversion CHECK. eauto using gwf_lex_refl. + + apply gwf_lex_lt; eauto. + rewrite !app_length. nia. + + apply gwf_lex_step; eauto. +Qed. + +Lemma gwf_add_cmp_right b: forall i j j' (LE: gwf_cmp b j j'), gwf_cmp b (i ++ j) (i ++ j'). +Proof. + intros. inversion LE; subst. + - apply gwf_cmp_lt. rewrite !app_length. nia. + - apply gwf_cmp_lex. + ginduction CMP; simpl; intros. + + destruct b; inversion CHECK. eauto using gwf_lex_refl. + + induction i0; simpl; eauto. + destruct a; eauto using bwfo_le_refl. + + induction i0; simpl; eauto. + destruct a; eauto using bwfo_le_refl. +Qed. + +Lemma gwf_acc_le: forall i j (WF: Acc (gwf_cmp false) i) (LE: gwf_cmp true j i), + Acc (gwf_cmp false) j. +Proof. + econstructor. intros. eapply WF. eauto using gwf_cmp_trans. +Qed. + +Lemma gwf_lt_bottom: forall i, gwf_cmp false i [] -> False. +Proof. + intros. inversion H; subst. + - inversion LEN. + - inversion CMP. inversion CHECK. +Qed. + +Lemma gwf_wf: well_founded (gwf_cmp false). +Proof. + cut (forall n i (LEon: length i <= n), Acc (gwf_cmp false) i). + { red; eauto. } + + induction n; intros. + { destruct i; inversion LEon. + econstructor. intros. exfalso. eauto using gwf_lt_bottom. } + destruct i. + { econstructor. intros. exfalso. eauto using gwf_lt_bottom. } + + destruct s as [o x]. revert i LEon. simpl. + assert (WFx := bwfo_wf _ x). + induction WFx as [x _ HYPx]. + econstructor. intros j LTj. + dependent destruction LTj. + { simpl in *. eapply IHn. nia. } + dependent destruction CMP. + { eapply HYPx; eauto. nia. } + + assert (WF: Acc (gwf_cmp false) i0). + { apply gwf_lex_length in CMP. eapply IHn. nia. } + revert x0 LE. induction WF as [j _ HYPj]. + econstructor. intros k LTk. + assert (LEN := gwf_lex_length CMP). + dependent destruction LTk. + { simpl in *. eapply IHn. nia. } + dependent destruction CMP0. + { eapply HYPx; eauto using bwfo_lt_le_lt. nia. } + eapply HYPj; eauto using bwfo_le_le_le. + eapply gwf_lex_trans; eauto; eauto. +Qed. + +Program Definition gwfo : awfo := + {| wfo_set := gwf_set; + wfo_le x y := gwf_cmp true x y; + wfo_lt x y := gwf_cmp false x y; + wfo_zero := nil; + wfo_one := gwf_one; + wfo_add x y := x ++ y; + |}. +Next Obligation. eauto using gwf_le_refl. Qed. +Next Obligation. eauto using gwf_le_refl. Qed. +Next Obligation. rewrite app_nil_r. eauto using gwf_le_refl. Qed. +Next Obligation. rewrite app_nil_r. eauto using gwf_le_refl. Qed. +Next Obligation. rewrite app_assoc. eauto using gwf_le_refl. Qed. +Next Obligation. rewrite app_assoc. eauto using gwf_le_refl. Qed. +Next Obligation. eauto using gwf_le_refl. Qed. +Next Obligation. eauto using gwf_lt_le. Qed. +Next Obligation. eauto using gwf_cmp_trans. Qed. +Next Obligation. eauto using gwf_cmp_trans. Qed. +Next Obligation. eauto using gwf_cmp_trans. Qed. +Next Obligation. eauto using gwf_add_cmp_left. Qed. +Next Obligation. eauto using gwf_add_cmp_right. Qed. +Next Obligation. eauto using gwf_add_cmp_left. Qed. +Next Obligation. eauto using gwf_add_cmp_right. Qed. +Next Obligation. eauto using gwf_wf. Qed. +Next Obligation. destruct i; eauto. econstructor. simpl. nia. Qed. + +(* ** + embedding and properties + *) + +Definition gwf_embed {o: bwfo} (a: o) : gwfo := + [ gwfel o a ]. + +Lemma gwf_embed_le_preserve (o: bwfo) (a b: o) + (LT: bwfo_le a b): + wfo_le (gwf_embed a) (gwf_embed b). +Proof. + repeat red. unfold gwf_embed. eauto. +Qed. + +Lemma gwf_embed_lt_preserve (o: bwfo) (a b: o) + (LT: bwfo_lt a b): + wfo_lt (gwf_embed a) (gwf_embed b). +Proof. + repeat red. unfold gwf_embed. eauto. +Qed. + +Lemma gwf_embed_reflect (o: bwfo) (a b: o) + (LT: wfo_lt (gwf_embed a) (gwf_embed b)): + bwfo_lt a b. +Proof. + repeat red in LT. unfold gwf_embed in *. dependent destruction LT; eauto. + - simpl in *. nia. + - dependent destruction CMP; eauto. + inversion CMP. inversion CHECK. +Qed. + +(* ** + Simple Properties about Orders + *) + +Lemma wfo_lt_neq: forall a i, ~ @wfo_lt a i i. +Proof. + intros. assert (WF := wfo_wf a i). red. + induction WF. eauto. +Qed. + +Lemma wfo_add_monotone: forall (a: awfo) (i i' j j': a) + (LEi: wfo_le i i') + (LEj: wfo_le j j'), + wfo_le (wfo_add i j) (wfo_add i' j'). +Proof. + eauto using wfo_le_le_le, wfo_add_le_left, wfo_add_le_right. +Qed. + +Lemma wfo_add_proj_left: forall a i j, @wfo_le a i (wfo_add i j). +Proof. + eauto using wfo_le_le_le, wfo_add_zero_r_ge, wfo_add_le_right, wfo_non_negative. +Qed. + +Lemma wfo_add_proj_right: forall a i j, @wfo_le a j (wfo_add i j). +Proof. + eauto using wfo_le_le_le, wfo_add_zero_l_ge, wfo_add_le_left, wfo_non_negative. +Qed. + +Lemma wfo_add_one: forall (a: awfo) (i: a), wfo_lt i (wfo_add wfo_one i). +Proof. + eauto using wfo_le_lt_lt, wfo_add_proj_right, wfo_add_lt_left, wfo_non_trivial. +Qed. + +(** [wfo_le_n n o o'] means that [o'] can be decreased at least [n] times + before reaching [o]. +*) +Inductive wfo_le_n {o: awfo} : nat -> o -> o -> Prop := +| wfo_le_n_Z i j (LE: wfo_le i j) + : wfo_le_n O i j +| wfo_le_n_S n i j k (GLE: wfo_le_n n i j) (LT: wfo_lt j k) + : wfo_le_n (S n) i k +. +Hint Constructors wfo_le_n. + +Lemma wfo_le_n_lt: forall o n (i i': wfo_set o) + (LE: wfo_le_n (S n) i i'), + wfo_lt i i'. +Proof. + induction n; intros; inversion LE; subst. + - inversion GLE; subst. eauto using wfo_le_lt_lt. + - apply IHn in GLE. eauto using wfo_lt_le, wfo_lt_le_lt. +Qed. + +(* TODO rename (D) *) +Lemma wfo_le_n_S': forall o n (i i': wfo_set o) + (LE: wfo_le_n (S n) i i'), + exists j : wfo_set o, + wfo_lt i j /\ + wfo_le_n n j i'. +Proof. + induction n; intros; inversion LE; subst. + - inversion GLE. subst. eauto using wfo_le_lt_lt, wfo_le_refl. + - edestruct IHn; eauto. + destruct H. eauto. +Qed. + +Lemma wfo_le_n_S'': forall o n (i i': wfo_set o) + (LE: wfo_le_n (S n) i i'), + wfo_le_n n i i'. +Proof. + intros; inversion LE; inversion GLE; subst; eauto using wfo_lt_le, wfo_le_le_le, wfo_lt_le_lt. +Qed. + +Lemma wfo_le_n_wfo_le: forall o n (i i' i'': wfo_set o) + (GLE: wfo_le_n n i i') + (LE: wfo_le i' i''), + wfo_le_n n i i''. +Proof. + intros; dependent destruction GLE; [econstructor 1|econstructor 2]; eauto using wfo_le_le_le, wfo_lt_le_lt. +Qed. + +Lemma wfo_le_n_anti: forall o m n (i i': wfo_set o) + (GLE: wfo_le_n m i i') + (LE: n <= m), + wfo_le_n n i i'. +Proof. + intros; ginduction LE; eauto. + intros; apply IHLE; auto using wfo_le_n_S''. +Qed. + +(* TODO rename *) +Lemma wfo_le_n_S_rev: forall o (i j: wfo_set o) n k + (LT: wfo_lt i j) + (GLE: wfo_le_n n j k), + wfo_le_n (S n) i k. +Proof. + intros; ginduction GLE; intros; eauto. + econstructor; eauto using wfo_lt_le_lt, wfo_le_refl. +Qed. + +Lemma wfo_le_n_plus: forall o n na nb (i i': wfo_set o) + (GLE: wfo_le_n n i i') + (E: n = na + nb), + exists ii, + wfo_le_n na i ii /\ + wfo_le_n nb ii i'. +Proof. + intros; ginduction na; simpl; intros; subst. + - exists i; eauto using wfo_le_refl. + - apply wfo_le_n_S' in GLE. destruct GLE as [? [? LE]]. + eapply IHna in LE; eauto. + destruct LE as [ii []]. + exists ii; eauto; split; eauto using wfo_le_n_S_rev. +Qed. + +(* ** + wfo_nat +*) + +Fixpoint wfo_nat {o : awfo} (n: nat) : wfo_set o := + match n with + | 0 => wfo_zero + | S n' => wfo_add wfo_one (wfo_nat n') + end. + +Lemma wfo_le_n_add: forall o n (i: wfo_set o), + wfo_le_n n i (wfo_add (wfo_nat n) i). +Proof. + induction n; eauto using wfo_add_lt_left, wfo_add_one, wfo_le_refl, wfo_add_proj_right. +Qed. + +Lemma wfo_nat_le_mon: forall o n m + (LE: n <= m), + @wfo_le o (wfo_nat n) (wfo_nat m). +Proof. + intros. induction LE; eauto using wfo_le_le_le, wfo_add_proj_right, wfo_le_refl. +Qed. + +Lemma wfo_nat_lt_mon: forall o n m + (LE: n < m), + @wfo_lt o (wfo_nat n) (wfo_nat m). +Proof. + intros; induction LE; eauto using wfo_lt_le_lt, wfo_lt_le, wfo_add_one. +Qed. diff --git a/theories/Eq/Eq.v b/theories/Eq/Eq.v index 8128c4a4..3c140b74 100644 --- a/theories/Eq/Eq.v +++ b/theories/Eq/Eq.v @@ -19,11 +19,14 @@ From Coq Require Import Program Setoid Morphisms - RelationClasses. + Relations + RelationClasses + Lia. From Paco Require Import paco. From ITree Require Import + Basics.GeneralWFO Basics.Basics Basics.HeterogeneousRelations Core.ITreeDefinition. @@ -40,8 +43,33 @@ Proof. auto. Qed. Global Instance Transitive_bot2 (A : Type) : @Transitive A bot2. Proof. auto. Qed. + (* end hide *) +Hint Resolve wfo_lt_le_lt wfo_le_lt_lt wfo_le_le_le wfo_add_lt_left wfo_add_lt_right wfo_add_le_left wfo_add_le_right wfo_add_monotone wfo_lt_le : wfo. +Hint Resolve wfo_add_proj_left wfo_add_proj_right : wfo_proj. +Hint Resolve wfo_le_refl : wfo_refl. + +Definition _tmp_id_ T (e: T) := e. + +Ltac unfold_eta := + repeat + match goal with + | |- context[@RetF ?a ?b ?c ?d] => + change (@RetF a b c d) with (observe (go ((@_tmp_id_ _ (@RetF)) a b c d))) + | H: context[@RetF ?a ?b ?c ?d] |- _ => + change (@RetF a b c d) with (observe (go ((@_tmp_id_ _ (@RetF)) a b c d))) in H + | |- context[@TauF ?a ?b ?c ?d] => + change (@TauF a b c d) with (observe (go ((@_tmp_id_ _ (@TauF)) a b c d))) + | H: context[@TauF ?a ?b ?c ?d] |- _ => + change (@TauF a b c d) with (observe (go ((@_tmp_id_ _ (@TauF)) a b c d))) in H + | |- context[@VisF ?a ?b ?c ?d ?e ?f] => + change (@VisF a b c d e f) with (observe (go ((@_tmp_id_ _ (@VisF)) a b c d e f))) + | H: context[@VisF ?a ?b ?c ?d ?e ?f] |- _ => + change (@VisF a b c d e f) with (observe (go ((@_tmp_id_ _ (@VisF)) a b c d e f))) in H + end; + unfold _tmp_id_ in *. + (** ** Coinductive reasoning with Paco *) (** Similarly to the way we deal with cofixpoints explained in @@ -64,7 +92,7 @@ Proof. auto. Qed. Coercion is_true : bool >-> Sortclass. -Section eqit. +Section eqit_Definition. (** Although the original motivation is to define an equivalence relation on [itree E R], we will generalize it into a @@ -75,8 +103,8 @@ Section eqit. Then the desired equivalence relation is obtained by setting [RR := eq] (with [R1 = R2]). *) - Context {E : Type -> Type} {R1 R2 : Type} (RR : R1 -> R2 -> Prop). - + Context {E : Type -> Type}. + (** We also need to do some gymnastics to work around the two-layered definition of [itree]. We first define a relation transformer [eqitF] as an indexed inductive type @@ -87,186 +115,219 @@ Section eqit. pattern-matching is not allowed on [itree]. *) - Inductive eqitF (b1 b2: bool) vclo (sim : itree E R1 -> itree E R2 -> Prop) : + Variant eqitF (b1 b2: bool) {R1 R2} (RR: R1->R2->Prop) (sim : gwfo -> itree E R1 -> itree E R2 -> Prop) (o: gwfo) : itree' E R1 -> itree' E R2 -> Prop := | EqRet r1 r2 - (REL: RR r1 r2): - eqitF b1 b2 vclo sim (RetF r1) (RetF r2) - | EqTau m1 m2 - (REL: sim m1 m2): - eqitF b1 b2 vclo sim (TauF m1) (TauF m2) + (REL: RR r1 r2) + : eqitF b1 b2 RR sim o (RetF r1) (RetF r2) | EqVis {u} (e : E u) k1 k2 - (REL: forall v, vclo sim (k1 v) (k2 v) : Prop): - eqitF b1 b2 vclo sim (VisF e k1) (VisF e k2) - | EqTauL t1 ot2 - (CHECK: b1) - (REL: eqitF b1 b2 vclo sim (observe t1) ot2): - eqitF b1 b2 vclo sim (TauF t1) ot2 - | EqTauR ot1 t2 + (REL: forall v, exists o', sim o' (k1 v) (k2 v)) + : eqitF b1 b2 RR sim o (VisF e k1) (VisF e k2) + | EqTau m1 m2 o' + (REL: sim o' m1 m2) + (LEo: wfo_le o' o) + : eqitF b1 b2 RR sim o (TauF m1) (TauF m2) + | EqTauL t1 t2 o' + (CHECK: b1) + (REL: sim o' t1 t2) + (LTo: wfo_lt o' o) + : eqitF b1 b2 RR sim o (TauF t1) (observe t2) + | EqTauR t1 t2 o' (CHECK: b2) - (REL: eqitF b1 b2 vclo sim ot1 (observe t2)): - eqitF b1 b2 vclo sim ot1 (TauF t2) + (REL: sim o' t1 t2) + (LTo: wfo_lt o' o) + : eqitF b1 b2 RR sim o (observe t1) (TauF t2) + | EqStutter t1 t2 o' + (CHECK1: b1) + (CHECK2: b2) + (REL: sim o' t1 t2) + (LTo: wfo_lt o' o) + : eqitF b1 b2 RR sim o (observe t1) (observe t2) . - Hint Constructors eqitF: core. - - Definition eqit_ b1 b2 vclo sim : - itree E R1 -> itree E R2 -> Prop := - fun t1 t2 => eqitF b1 b2 vclo sim (observe t1) (observe t2). - Hint Unfold eqit_: core. - - (** [eqitF] and [eqit_] are both monotone. *) - - Lemma eqitF_mono b1 b2 x0 x1 vclo vclo' sim sim' - (IN: eqitF b1 b2 vclo sim x0 x1) - (MON: monotone2 vclo) - (LEc: vclo <3= vclo') - (LE: sim <2= sim'): - eqitF b1 b2 vclo' sim' x0 x1. - Proof. - intros. induction IN; eauto. - Qed. - - Lemma eqit__mono b1 b2 vclo (MON: monotone2 vclo) : monotone2 (eqit_ b1 b2 vclo). - Proof. do 2 red. intros. eapply eqitF_mono; eauto. Qed. + + Definition eqit_ b1 b2 + (sim: forall {R1 R2},(R1->R2->Prop)-> gwfo -> itree E R1 -> itree E R2 -> Prop) + R1 R2 (RR: R1->R2->Prop) o t1 t2 := + eqitF b1 b2 RR (sim RR) o (observe t1) (observe t2). - Hint Resolve eqit__mono : paco. + Definition eqiti b1 b2 {R1 R2} RR o t1 t2 := + paco6 (eqit_ b1 b2) bot6 R1 R2 RR o t1 t2. - Lemma eqit_idclo_mono: monotone2 (@id (itree E R1 -> itree E R2 -> Prop)). - Proof. unfold id. eauto. Qed. + Definition eqitz b1 b2 {R1 R2} RR t1 t2 := @eqiti b1 b2 R1 R2 RR wfo_zero t1 t2. - Hint Resolve eqit_idclo_mono : paco. - - Definition eqit b1 b2 : itree E R1 -> itree E R2 -> Prop := - paco2 (eqit_ b1 b2 id) bot2. + Variant eqit b1 b2 {R1 R2} RR t1 t2 : Prop := + | eqit_exists o (REL: @eqiti b1 b2 R1 R2 RR o t1 t2) + . - (** Strong bisimulation on itrees. If [eqit RR t1 t2], + (** Strong bisimulation on itrees. If [eq_itree RR t1 t2], we say that [t1] and [t2] are (strongly) bisimilar. As hinted at above, bisimilarity can be intuitively thought of as equality. *) - Definition eq_itree := eqit false false. + Definition eq_itree {R1 R2} := @eqit false false R1 R2. - Definition eutt := eqit true true. + Definition eutt {R1 R2} := @eqit true true R1 R2. - Definition euttge := eqit true false. + Definition euttge {R1 R2} := @eqit true false R1 R2. + +End eqit_Definition. -End eqit. - -(* begin hide *) Hint Constructors eqitF: core. Hint Unfold eqit_: core. -Hint Resolve eqit__mono : paco. -Hint Resolve eqit_idclo_mono : paco. -Hint Unfold eqit: core. +Hint Unfold eqiti : core. +Hint Unfold eqitz : core. +Hint Constructors eqit: core. Hint Unfold eq_itree: core. Hint Unfold eutt: core. Hint Unfold euttge: core. Hint Unfold id: core. +Section eqit_Properties. + + Context {E : Type -> Type}. + + (** [eqitF] and [eqit_] are both monotone. *) + + Lemma eqitF_mono R1 R2 RR RR' b1 b2 o o' x0 x1 sim sim' + (IN: @eqitF E b1 b2 R1 R2 RR sim o x0 x1) + (LER: RR <2= RR') + (LE: sim <3= sim') + (LEo: wfo_le o o'): + eqitF b1 b2 RR' sim' o' x0 x1. + Proof. + inv IN; eauto using wfo_lt_le_lt, wfo_le_le_le. + econstructor. intros. destruct (REL v). eauto. + Qed. + + Lemma eqit__mono b1 b2: monotone6 (@eqit_ E b1 b2). + Proof. + red; intros. eapply eqitF_mono; eauto using wfo_le_refl. + Qed. + +End eqit_Properties. + +Hint Resolve eqit__mono : paco. + +(* begin hide *) + Ltac unfold_eqit := - (try match goal with [|- eqit_ _ _ _ _ _ _ _ ] => red end); - (repeat match goal with [H: eqit_ _ _ _ _ _ _ _ |- _ ] => red in H end). + (try match goal with [|- eqit_ _ _ _ _ _ _ _ _ _] => red end); + (repeat match goal with [H: eqit_ _ _ _ _ _ _ _ _ _|- _ ] => red in H end). + +Ltac fold_eqit := + (try match goal with [|- eqitF ?b1 ?b2 ?RR (?sim _ _ _) ?o (observe ?t1) (observe ?t2)] + => fold (eqit_ b1 b2 sim _ _ RR o t1 t2) + end); + (repeat match goal with [H: eqitF ?b1 ?b2 ?RR (?sim _ _ _) ?o (observe ?t1) (observe ?t2) |- _] + => fold (eqit_ b1 b2 sim _ _ RR o t1 t2) in H + end). Lemma fold_eqitF: - forall {E R1 R2} (RR: R1 -> R2 -> Prop) b1 b2 (t1 : itree E R1) (t2 : itree E R2) ot1 ot2, - eqitF RR b1 b2 id (upaco2 (eqit_ RR b1 b2 id) bot2) ot1 ot2 -> + forall {E R1 R2} (RR: R1 -> R2 -> Prop) b1 b2 (t1 : itree E R1) (t2 : itree E R2) o ot1 ot2, + eqitF b1 b2 RR (upaco6 (eqit_ b1 b2) bot6 _ _ RR) o ot1 ot2 -> ot1 = observe t1 -> ot2 = observe t2 -> - eqit RR b1 b2 t1 t2. -Proof. - intros * eq -> ->; pfold; auto. -Qed. - -Instance eqitF_Proper_R {E : Type -> Type} {R1 R2:Type} : - Proper ((@eq_rel R1 R2) ==> eq ==> eq ==> (eq_rel ==> eq_rel) ==> eq_rel ==> eq_rel) - (@eqitF E R1 R2). -Proof. - repeat red. - intros. subst. split; unfold subrelationH; intros. - - induction H0; try auto. - econstructor. apply H. assumption. - econstructor. apply H3. assumption. - econstructor. intros. specialize (REL v). specialize (H2 x3 y3). apply H2 in H3. apply H3. assumption. - - induction H0; try auto. - econstructor. apply H. assumption. - econstructor. apply H3. assumption. - econstructor. intros. specialize (REL v). specialize (H2 x3 y3). apply H2 in H3. apply H3. assumption. -Qed. - -Instance eqitF_Proper_R2 {E : Type -> Type} {R1 R2:Type} : - Proper ((@eq_rel R1 R2) ==> eq ==> eq ==> eq ==> eq ==> eq ==> eq ==> iff) - (@eqitF E R1 R2). -Proof. - repeat red. - intros. subst. split; intros. - - induction H0; try auto. - econstructor. apply H. assumption. - - induction H0; try auto. - econstructor. apply H. assumption. -Qed. - -Instance eqit_Proper_R {E : Type -> Type} {R1 R2:Type} - : Proper ( (@eq_rel R1 R2) ==> eq ==> eq ==> eq ==> eq ==> iff) (@eqit E R1 R2). -Proof. - repeat red. - intros. subst. - split. - - revert_until y1. pcofix CIH. intros. - pstep. punfold H1. red in H1. red. - hinduction H1 before CIH; intros; eauto. - + apply EqRet. apply H. assumption. - + apply EqTau. right. apply CIH. pclearbot. pinversion REL. - + apply EqVis. intros. red. right. apply CIH. - specialize (REL v). - red in REL. pclearbot. pinversion REL. - - revert_until y1. pcofix CIH. intros. - pstep. punfold H1. red in H1. red. - hinduction H1 before CIH; intros; eauto. - + apply EqRet. apply H. assumption. - + apply EqTau. right. apply CIH. pclearbot. pinversion REL. - + apply EqVis. intros. red. right. apply CIH. - specialize (REL v). - red in REL. pclearbot. pinversion REL. + eqit b1 b2 RR t1 t2. +Proof. + intros * eq -> ->. eexists. pfold. eauto. Qed. -Instance eutt_Proper_R {E : Type -> Type} {R1 R2:Type} - : Proper ( (@eq_rel R1 R2) ==> eq ==> eq ==> iff) (@eutt E R1 R2). +Definition eqit_rel_flip {E} + (r: forall R1 R2,(R1->R2->Prop)-> gwfo -> itree E R1 -> itree E R2 -> Prop) + R1 R2 RR o t1 t2 := + r R2 R1 (flip RR) o t2 t1. + +Lemma eqitF_flip {E R1 R2} (RR : R1 -> R2 -> Prop) b1 b2 r: + (fun o => flip (eqitF b2 b1 (flip RR) (fun o => flip (r o)) o)) <3= @eqitF E b1 b2 R1 R2 RR r. Proof. - unfold eutt. repeat red. - intros. split; intros; subst. - - rewrite <- H. assumption. - - rewrite H. assumption. + intros. destruct PR; eauto. Qed. +Lemma eqiti_r_flip E (r: forall R1 R2,(R1->R2->Prop)-> gwfo -> itree E R1 -> itree E R2 -> Prop) R1 R2 RR b1 b2 + (u : itree E R1) (v : itree E R2) o + (REL: paco6 (eqit_ b2 b1) (eqit_rel_flip r) R2 R1 (flip RR) o v u) + : paco6 (eqit_ b1 b2) r R1 R2 RR o u v. +Proof. + intros. revert_until b2. pcofix self. pstep; intros. punfold REL. + red. inv REL; econstructor; eauto; intros; edestruct REL0; eauto. + destruct H1; eauto. +Qed. -Definition flip_clo {A B C} clo r := @flip A B C (clo (@flip B A C r)). - -Lemma eqitF_flip {E R1 R2} (RR : R1 -> R2 -> Prop) b1 b2 vclo r: - flip (eqitF (flip RR) b2 b1 (flip_clo vclo) (flip r)) <2= @eqitF E R1 R2 RR b1 b2 vclo r. +Lemma eqiti_flip E R1 R2 RR b1 b2: + forall (u : itree E R1) (v : itree E R2) o, + eqiti b2 b1 (flip RR) o v u -> eqiti b1 b2 RR o u v. Proof. - intros. induction PR; eauto. + eauto using eqiti_r_flip. Qed. -Lemma eqit_flip {E R1 R2} (RR : R1 -> R2 -> Prop) b1 b2: +Lemma eqit_flip E R1 R2 RR b1 b2: forall (u : itree E R1) (v : itree E R2), - eqit (flip RR) b2 b1 v u -> eqit RR b1 b2 u v. + eqit b2 b1 (flip RR) v u -> eqit b1 b2 RR u v. Proof. - pcofix self; pstep. intros u v euv. punfold euv. - red in euv |- *. induction euv; pclearbot; eauto 7 with paco. + intros. destruct H. eauto using eqiti_flip. Qed. -Lemma eqit_mon {E R1 R2} RR RR' (b1 b2 b1' b2': bool) +Lemma eqiti_mon E R1 R2 RR RR' (b1 b2 b1' b2': bool) o o' t1 t2 + (REL: @eqiti E b1 b2 R1 R2 RR o t1 t2) (LEb1: b1 -> b1') (LEb2: b2 -> b2') + (LEo: wfo_le o o') (LERR: RR <2= RR'): - @eqit E R1 R2 RR b1 b2 <2= eqit RR' b1' b2'. + eqiti b1' b2' RR' o' t1 t2. Proof. - pcofix self. pstep. intros u v euv. punfold euv. - red in euv |- *. induction euv; pclearbot; eauto 7 with paco. + intros. revert o o' LEo t1 t2 REL. pcofix self. intros. pstep. punfold REL. + red. inv REL; pclearbot; econstructor; eauto using wfo_lt_le_lt, wfo_le_refl. + intros. destruct (REL0 v). pclearbot. eauto 7 using wfo_le_refl. +Qed. + +Lemma eqit_mon E R1 R2 RR RR' (b1 b2 b1' b2': bool) t1 t2 + (REL: @eqit E b1 b2 R1 R2 RR t1 t2) + (LEb1: b1 -> b1') + (LEb2: b2 -> b2') + (LERR: RR <2= RR'): + eqit b1' b2' RR' t1 t2. +Proof. + intros. destruct REL. exists o. + eapply eqiti_mon; eauto using wfo_le_refl. Qed. Hint Unfold flip: core. +Instance eqitF_Proper_R {E : Type -> Type} b1 b2 {R1 R2:Type} : + Proper ((@eq_rel R1 R2) ==> (eq ==> eq_rel) ==> eq ==> eq_rel) + (@eqitF E b1 b2 R1 R2). +Proof. + repeat red. intros. subst. split; red; intros. + - eapply eqitF_mono; intros; eauto using wfo_le_refl. eapply H; eauto. eapply H0; eauto. + - eapply eqitF_mono; intros; eauto using wfo_le_refl. eapply H; eauto. eapply H0; eauto. +Qed. + +Instance eqitF_Proper_R2 {E : Type -> Type} b1 b2 {R1 R2:Type} : + Proper ((@eq_rel R1 R2) ==> eq ==> eq ==> eq ==> eq ==> iff) + (@eqitF E b1 b2 R1 R2). +Proof. + repeat red. intros. subst. split; intros. + - eapply eqitF_mono; intros; eauto using wfo_le_refl. eapply H; eauto. + - eapply eqitF_mono; intros; eauto using wfo_le_refl. eapply H; eauto. +Qed. + +Instance eqit_Proper_R {E : Type -> Type} b1 b2 R1 R2 + : Proper ((@eq_rel R1 R2) ==> eq ==> eq ==> iff) (@eqit E b1 b2 R1 R2). +Proof. + unfold eq_rel. repeat red. intros. subst. + destruct H. unfold subrelationH in *. + eauto using eqit_mon. +Qed. + +Instance eutt_Proper_R {E : Type -> Type} {R1 R2:Type} + : Proper ( (@eq_rel R1 R2) ==> eq ==> eq ==> iff) (@eutt E R1 R2). +Proof. + unfold eutt. repeat red. intros. subst. + destruct H. unfold subrelationH in *. + eauto using eqit_mon. +Qed. + + (* end hide *) (* @@ -279,261 +340,242 @@ Delimit Scope eq_itree_scope with eq_itree. tex-mode *) Open Scope itree. - + Infix "≅" := (eq_itree eq) (at level 70) : itree_scope. Infix "≈" := (eutt eq) (at level 70) : itree_scope. Infix "≳" := (euttge eq) (at level 70) : itree_scope. -Section eqit_closure. - -Context {E : Type -> Type} {R1 R2 : Type} (RR : R1 -> R2 -> Prop). +Hint Resolve cpn6_wcompat : core. -(** *** "Up-to" principles for coinduction. *) +(** ** Properties of relations *) -Inductive eqit_trans_clo b1 b2 b1' b2' (r : itree E R1 -> itree E R2 -> Prop) - : itree E R1 -> itree E R2 -> Prop := -| eqit_trans_clo_intro t1 t2 t1' t2' RR1 RR2 - (EQVl: eqit RR1 b1 b1' t1 t1') - (EQVr: eqit RR2 b2 b2' t2 t2') - (REL: r t1' t2') - (LERR1: forall x x' y, RR1 x x' -> RR x' y -> RR x y) - (LERR2: forall x y y', RR2 y y' -> RR x y' -> RR x y) - : eqit_trans_clo b1 b2 b1' b2' r t1 t2 -. -Hint Constructors eqit_trans_clo: core. +(** Instances stating that we have equivalence relations. *) -Definition eqitC b1 b2 := eqit_trans_clo b1 b2 false false. -Hint Unfold eqitC: core. +Section eqit_gen. -Lemma eqitC_mon b1 b2 r1 r2 t1 t2 - (IN: eqitC b1 b2 r1 t1 t2) - (LE: r1 <2= r2): - eqitC b1 b2 r2 t1 t2. -Proof. - destruct IN. econstructor; eauto. -Qed. +(** *** Properties of relation transformers. *) -Hint Resolve eqitC_mon : paco. +Context {E : Type -> Type}. -Lemma eqitC_wcompat b1 b2 vclo - (MON: monotone2 vclo) - (CMP: compose (eqitC b1 b2) vclo <3= compose vclo (eqitC b1 b2)): - wcompatible2 (@eqit_ E R1 R2 RR b1 b2 vclo) (eqitC b1 b2). +Global Instance Reflexive_eqitF b1 b2 {R: Type} (RR : R -> R -> Prop) sim + : Reflexive RR -> (forall o, Reflexive (sim o)) -> + forall o, Reflexive (@eqitF E b1 b2 _ _ RR sim o). Proof. - econstructor. pmonauto. - intros. dependent destruction PR. - punfold EQVl. punfold EQVr. unfold_eqit. - hinduction REL before r; intros; clear t1' t2'. - - remember (RetF r1) as x. - hinduction EQVl before r; intros; subst; try inv Heqx; eauto. - remember (RetF r3) as y. - hinduction EQVr before r; intros; subst; try inv Heqy; eauto. - - remember (TauF m1) as x. - hinduction EQVl before r; intros; subst; try inv Heqx; try inv CHECK; eauto. - remember (TauF m3) as y. - hinduction EQVr before r; intros; subst; try inv Heqy; try inv CHECK; eauto. - pclearbot. econstructor. gclo. - econstructor; cycle -1; eauto with paco. - - remember (VisF e k1) as x. - hinduction EQVl before r; intros; subst; try dependent destruction Heqx; try inv CHECK; eauto. - remember (VisF e0 k3) as y. - hinduction EQVr before r; intros; subst; try dependent destruction Heqy; try inv CHECK; eauto. - econstructor. intros. pclearbot. - eapply MON. - + apply CMP. econstructor; eauto. - + intros. apply gpaco2_clo, PR. - - remember (TauF t1) as x. - hinduction EQVl before r; intros; subst; try inv Heqx; try inv CHECK; eauto. - pclearbot. punfold REL. - - remember (TauF t2) as y. - hinduction EQVr before r; intros; subst; try inv Heqy; try inv CHECK; eauto. - pclearbot. punfold REL. + red; intros. red in H0. destruct x; eauto using wfo_le_refl. + Grab Existential Variables. eauto. Qed. -Hint Resolve eqitC_wcompat : paco. - -Lemma eqit_idclo_compat b1 b2: compose (eqitC b1 b2) id <3= compose id (eqitC b1 b2). +Global Instance Symmetric_eqitF b {R: Type} (RR : R -> R -> Prop) sim + : Symmetric RR -> (forall o, Symmetric (sim o)) -> + forall o, Symmetric (@eqitF E b b _ _ RR sim o). Proof. - intros. apply PR. + red; intros. red in H0. dependent destruction H1; eauto. + econstructor. intros. destruct (REL v). eauto. Qed. -Hint Resolve eqit_idclo_compat : paco. -Lemma eqitC_dist b1 b2: - forall r1 r2, eqitC b1 b2 (r1 \2/ r2) <2= (eqitC b1 b2 r1 \2/ eqitC b1 b2 r2). +Global Instance Reflexive_eqit_ b1 b2 R (RR: R->R->Prop) (sim: forall R1 R2,(R1->R2->Prop)->_->_->_->Prop) + : Reflexive RR -> + (forall o, Reflexive (sim R R RR o)) -> + forall o, Reflexive (@eqit_ E b1 b2 sim R R RR o). Proof. - intros. destruct PR. destruct REL; eauto. + red. intros. eapply Reflexive_eqitF; eauto. Qed. -Hint Resolve eqitC_dist : paco. - -Lemma eqit_clo_trans b1 b2 vclo - (MON: monotone2 vclo) - (CMP: compose (eqitC b1 b2) vclo <3= compose vclo (eqitC b1 b2)): - eqit_trans_clo b1 b2 false false <3= gupaco2 (eqit_ RR b1 b2 vclo) (eqitC b1 b2). +Global Instance Symmetric_eqit_ b R (RR: R->R->Prop) (sim: forall R1 R2,(R1->R2->Prop)->_->_->_->Prop) + : Symmetric RR -> + (forall o, Symmetric (sim R R RR o)) -> + forall o, Symmetric (@eqit_ E b b sim R R RR o). Proof. - intros. destruct PR. gclo. econstructor; eauto with paco. + red. intros. eapply Symmetric_eqitF; eauto. Qed. -End eqit_closure. - -Hint Unfold eqitC: core. -Hint Resolve eqitC_mon : paco. -Hint Resolve eqitC_wcompat : paco. -Hint Resolve eqit_idclo_compat : paco. -Hint Resolve eqitC_dist : paco. -Arguments eqit_clo_trans : clear implicits. -Hint Constructors eqit_trans_clo: core. - -(** ** Properties of relations *) - -(** Instances stating that we have equivalence relations. *) - -Section eqit_gen. - -(** *** Properties of relation transformers. *) - -Context {E : Type -> Type} {R: Type} (RR : R -> R -> Prop). +(** *** [eqit] is an equivalence relation *) -Global Instance Reflexive_eqitF b1 b2 (sim : itree E R -> itree E R -> Prop) -: Reflexive RR -> Reflexive sim -> Reflexive (eqitF RR b1 b2 id sim). +Global Instance Reflexive_eqit_gen b1 b2 r rg R (RR:R->R->Prop) o + : Reflexive RR -> + Reflexive (gpaco6 (@eqit_ E b1 b2) (cpn6 (eqit_ b1 b2)) r rg R R RR o). Proof. - red. destruct x; constructor; eauto. + gcofix CIH. gstep; intros. + repeat red. destruct (observe x); eauto using wfo_le_refl with paco. Qed. -Global Instance Symmetric_eqitF b (sim : itree E R -> itree E R -> Prop) -: Symmetric RR -> Symmetric sim -> Symmetric (eqitF RR b b id sim). +Global Instance Reflexive_eqiti b1 b2 R (RR:R->R->Prop) o + : Reflexive RR -> Reflexive (@eqiti E b1 b2 R R RR o). Proof. - red. induction 3; constructor; subst; eauto. - intros. apply H0. apply (REL v). + ginit. intros. apply Reflexive_eqit_gen; eauto. Qed. -Global Instance Reflexive_eqit_ b1 b2 (sim : itree E R -> itree E R -> Prop) -: Reflexive RR -> Reflexive sim -> Reflexive (eqit_ RR b1 b2 id sim). -Proof. repeat red. intros. reflexivity. Qed. - -Global Instance Symmetric_eqit_ b (sim : itree E R -> itree E R -> Prop) -: Symmetric RR -> Symmetric sim -> Symmetric (eqit_ RR b b id sim). -Proof. repeat red; symmetry; auto. Qed. - -(** *** [eqit] is an equivalence relation *) - -Global Instance Reflexive_eqit_gen b1 b2 (r rg: itree E R -> itree E R -> Prop) : - Reflexive RR -> Reflexive (gpaco2 (eqit_ RR b1 b2 id) (eqitC RR b1 b2) r rg). +Global Instance Reflexive_eqit b1 b2 R (RR:R->R->Prop) + : Reflexive RR -> Reflexive (@eqit E b1 b2 R R RR). Proof. - gcofix CIH. gstep; intros. - repeat red. destruct (observe x); eauto with paco. + econstructor. apply Reflexive_eqiti. eauto. + Grab Existential Variables. eapply wfo_zero. Qed. -Global Instance Reflexive_eqit b1 b2 : Reflexive RR -> Reflexive (@eqit E _ _ RR b1 b2). +Global Instance Symmetric_eqiti b R (RR:R->R->Prop) o + : Symmetric RR -> Symmetric (@eqiti E b b R R RR o). Proof. - red; intros. ginit. apply Reflexive_eqit_gen; eauto. + red; intros. apply eqiti_flip. + eapply eqiti_mon; eauto using wfo_le_refl. Qed. -Global Instance Symmetric_eqit b : Symmetric RR -> Symmetric (@eqit E _ _ RR b b). +Global Instance Symmetric_eqit b R (RR:R->R->Prop) + : Symmetric RR -> Symmetric (@eqit E b b R R RR). Proof. - red; intros. apply eqit_flip. - eapply eqit_mon, H0; eauto. + red. intros. destruct H0. exists o. + apply Symmetric_eqiti; eauto. Qed. -Global Instance eq_sub_euttge: - subrelation (@eq_itree E _ _ RR) (euttge RR). +Global Instance eq_sub_euttge R RR + : subrelation (@eq_itree E R R RR) (euttge RR). Proof. - ginit. gcofix CIH. intros. - punfold H0. gstep. red in H0 |- *. - hinduction H0 before CIH; subst; econstructor; try inv CHECK; pclearbot; eauto 7 with paco. + red; intros. destruct H. exists o. + ginit. revert_until E. + gcofix CIH. intros. + punfold REL. gstep. + red in REL |- *. + inv REL; pclearbot; eauto 7 with paco. + econstructor. intros. destruct (REL0 v). pclearbot. eauto with paco. Qed. -Global Instance euttge_sub_eutt: - subrelation (@euttge E _ _ RR) (eutt RR). +Global Instance euttge_sub_eutt R RR + : subrelation (@euttge E R R RR) (eutt RR). Proof. - ginit. gcofix CIH. intros. - punfold H0. gstep. red in H0 |- *. - hinduction H0 before CIH; subst; econstructor; pclearbot; eauto 7 with paco. + red; intros. destruct H. exists o. + ginit. revert_until E. + gcofix CIH. intros. + punfold REL. gstep. + red in REL |- *. + inv REL; pclearbot; eauto 7 with paco. + econstructor. intros. destruct (REL0 v). pclearbot. eauto with paco. Qed. -Global Instance eq_sub_eutt: - subrelation (@eq_itree E _ _ RR) (eutt RR). +Global Instance eq_sub_eutt R RR + : subrelation (@eq_itree E R R RR) (eutt RR). Proof. red; intros. eapply euttge_sub_eutt. eapply eq_sub_euttge. apply H. Qed. End eqit_gen. -Hint Resolve Reflexive_eqit Reflexive_eqit_gen : reflexivity. +Hint Resolve Reflexive_eqit Reflexive_eqiti Reflexive_eqit_gen : reflexivity. Section eqit_eq. (** *** Properties of relation transformers. *) -Context {E : Type -> Type} {R : Type}. - -Local Notation eqit := (@eqit E R R eq). +Context {E : Type -> Type} {R: Type}. -Global Instance Reflexive_eqitF_eq b1 b2 (sim : itree E R -> itree E R -> Prop) -: Reflexive sim -> Reflexive (eqitF eq b1 b2 id sim). +Global Instance Reflexive_eqitF_eq b1 b2 sim + : (forall o, Reflexive (sim o)) -> + forall o, Reflexive (@eqitF E b1 b2 R R eq sim o). Proof. apply Reflexive_eqitF; eauto. Qed. -Global Instance Symmetric_eqitF_eq b (sim : itree E R -> itree E R -> Prop) -: Symmetric sim -> Symmetric (eqitF eq b b id sim). +Global Instance Symmetric_eqitF_eq b sim + : (forall o, Symmetric (sim o)) -> + forall o, Symmetric (@eqitF E b b R R eq sim o). Proof. apply Symmetric_eqitF; eauto. Qed. -Global Instance Reflexive_eqit__eq b1 b2 (sim : itree E R -> itree E R -> Prop) -: Reflexive sim -> Reflexive (eqit_ eq b1 b2 id sim). -Proof. apply Reflexive_eqit_; eauto. Qed. +Global Instance Reflexive_eqit__eq b1 b2 (sim: forall R1 R2,(R1->R2->Prop)->_->_->_->_) + : (forall o, Reflexive (sim R R eq o)) -> + forall o, Reflexive (@eqit_ E b1 b2 sim R R eq o). +Proof. intros. eapply Reflexive_eqit_; eauto. Qed. -Global Instance Symmetric_eqit__eq b (sim : itree E R -> itree E R -> Prop) -: Symmetric sim -> Symmetric (eqit_ eq b b id sim). +Global Instance Symmetric_eqit__eq b (sim: forall R1 R2,(R1->R2->Prop)->_->_->_->_) + : (forall o, Symmetric (sim R R eq o)) -> + forall o, Symmetric (@eqit_ E b b sim R R eq o). Proof. apply Symmetric_eqit_; eauto. Qed. (** *** [eqit] is an equivalence relation *) -Global Instance Reflexive_eqit_gen_eq b1 b2 (r rg: itree E R -> itree E R -> Prop) : - Reflexive (gpaco2 (eqit_ eq b1 b2 id) (eqitC eq b1 b2) r rg). +Global Instance Reflexive_eqit_gen_eq b1 b2 r rg + : forall o, Reflexive (gpaco6 (@eqit_ E b1 b2) (cpn6 (eqit_ b1 b2)) r rg R R eq o). Proof. - apply Reflexive_eqit_gen; eauto. + intros. apply Reflexive_eqit_gen; eauto. Qed. -Global Instance Reflexive_eqit_eq b1 b2 : Reflexive (eqit b1 b2). +Global Instance Reflexive_eqiti_eq b1 b2 o + : Reflexive (@eqiti E b1 b2 R R eq o). +Proof. + apply Reflexive_eqiti; eauto. +Qed. + +Global Instance Reflexive_eqit_eq b1 b2 + : Reflexive (@eqit E b1 b2 R R eq). Proof. apply Reflexive_eqit; eauto. Qed. -Global Instance Symmetric_eqit_eq b : Symmetric (eqit b b). +Global Instance Symmetric_eqiti_eq b o + : Symmetric (@eqiti E b b R R eq o). +Proof. + apply Symmetric_eqiti; eauto. +Qed. + +Global Instance Symmetric_eqit_eq b + : Symmetric (@eqit E b b R R eq). Proof. apply Symmetric_eqit; eauto. Qed. (** *** Congruence properties *) +Global Instance eqiti_observe b1 b2 o: + Proper (eqiti b1 b2 eq o ==> going (eqiti b1 b2 eq o)) (@observe E R). +Proof. + constructor. punfold H. +Qed. + Global Instance eqit_observe b1 b2: - Proper (eqit b1 b2 ==> going (eqit b1 b2)) (@observe E R). + Proper (eqit b1 b2 eq ==> going (eqit b1 b2 eq)) (@observe E R). +Proof. + constructor. destruct H. exists o. punfold REL. +Qed. + +Global Instance eqiti_tauF b1 b2 o: + Proper (eqiti b1 b2 eq o ==> going (eqiti b1 b2 eq o)) (@TauF E R _). Proof. - constructor; punfold H. + constructor. pstep. econstructor; eauto using wfo_le_refl. Qed. Global Instance eqit_tauF b1 b2: - Proper (eqit b1 b2 ==> going (eqit b1 b2)) (@TauF E R _). + Proper (eqit b1 b2 eq ==> going (eqit b1 b2 eq)) (@TauF E R _). +Proof. + constructor. destruct H. exists o. pstep. econstructor; eauto using wfo_le_refl. +Qed. + +Global Instance eqiti_visF b1 b2 o {u} (e: E u): + Proper (pointwise_relation _ (eqiti b1 b2 (@eq R) o) ==> going (eqiti b1 b2 eq o)) (VisF e). Proof. - constructor; pstep. econstructor. eauto. + econstructor. pstep. + econstructor. intros. specialize (H v). eauto. Qed. -Global Instance eqit_VisF b1 b2 {u} (e: E u) : - Proper (pointwise_relation _ (eqit b1 b2) ==> going (eqit b1 b2)) (VisF e). +Global Instance eqit_visF b1 b2 {u} (e: E u) : + Proper (pointwise_relation _ (eqit b1 b2 (@eq R)) ==> going (eqit b1 b2 eq)) (VisF e). Proof. - constructor; red in H. unfold eqit in *. pstep; econstructor; eauto. + econstructor. exists wfo_zero. pstep. + econstructor. intros. destruct (H v). eauto. Qed. -Global Instance observing_sub_eqit l r : - subrelation (observing eq) (eqit l r). +Global Instance observing_sub_eqiti b1 b2 o : + subrelation (observing eq) (@eqiti E b1 b2 R R eq o). Proof. - repeat red; intros. destruct H. - pstep. red. rewrite H. apply Reflexive_eqitF; eauto. left. apply reflexivity. + repeat red; intros. pstep. red. rewrite H. + apply Reflexive_eqitF; eauto. + intros. left. apply Reflexive_eqiti. eauto. +Qed. + +Global Instance observing_sub_eqit b1 b2 : + subrelation (observing eq) (@eqit E b1 b2 R R eq). +Proof. + exists wfo_zero. eapply observing_sub_eqiti. eauto. Qed. (** ** Eta-expansion *) @@ -551,166 +593,229 @@ End eqit_eq. Lemma eq_itree_inv_ret {E R} (t : itree E R) r : t ≅ (Ret r) -> observe t = RetF r. Proof. - intros; punfold H; inv H; try inv CHECK; eauto. + intros. destruct H. punfold REL. inv REL; try inv CHECK; try inv CHECK1; try inv CHECK2; eauto. Qed. Lemma eq_itree_inv_vis {E R U} (t : itree E R) (e : E U) (k : U -> _) : t ≅ Vis e k -> exists k', observe t = VisF e k' /\ forall u, k' u ≅ k u. Proof. - intros; punfold H; inv H; auto_inj_pair2; subst; try inv CHECK. + intros. destruct H. punfold REL; inv REL; auto_inj_pair2; subst; try inv CHECK; try inv CHECK1; try inv CHECK2. eexists; split; eauto. - intros. destruct (REL u); try contradiction; pclearbot; eauto. + intros. destruct (REL0 u); try contradiction; pclearbot; eauto. Qed. Lemma eq_itree_inv_tau {E R} (t t' : itree E R) : t ≅ Tau t' -> exists t0, observe t = TauF t0 /\ t0 ≅ t'. Proof. - intros; punfold H; inv H; try inv CHECK; pclearbot; eauto. + intros; destruct H. punfold REL; inv REL; try inv CHECK; try inv CHECK1; try inv CHECK2; pclearbot; eauto. Qed. Lemma eqit_inv_ret {E R1 R2 RR} b1 b2 r1 r2 : - @eqit E R1 R2 RR b1 b2 (Ret r1) (Ret r2) -> RR r1 r2. + @eqit E b1 b2 R1 R2 RR (Ret r1) (Ret r2) -> RR r1 r2. Proof. - intros. punfold H. inv H. eauto. + intros. destruct H as [? H]. + assert (WFo := wfo_wf _ o). induction WFo. + punfold H. inv H; eauto. + eapply H1; eauto. + pclearbot. rewrite <-H3, <-H4. punfold REL. Qed. Lemma eqit_inv_vis {E R1 R2 RR} b1 b2 {u} (e1 e2: E u) (k1: u -> itree E R1) (k2: u -> itree E R2) : - eqit RR b1 b2 (Vis e1 k1) (Vis e2 k2) -> e1 = e2 /\ (forall u, eqit RR b1 b2 (k1 u) (k2 u)). -Proof. - intros. punfold H. repeat red in H. simpl in H. - dependent destruction H. pclearbot. eauto. -Qed. - -Lemma eqit_inv_tauL {E R1 R2 RR} b1 t1 t2 : - @eqit E R1 R2 RR b1 true (Tau t1) t2 -> eqit RR b1 true t1 t2. -Proof. - intros. punfold H. red in H. simpl in *. - remember (TauF t1) as tt1. genobs t2 ot2. - hinduction H before b1; intros; try discriminate. - - inv Heqtt1. pclearbot. pstep. red. simpobs. econstructor; eauto. pstep_reverse. - - inv Heqtt1. punfold_reverse H. - - red in IHeqitF. pstep. red; simpobs. econstructor; eauto. pstep_reverse. -Qed. - -Lemma eqit_inv_tauR {E R1 R2 RR} b2 t1 t2 : - @eqit E R1 R2 RR true b2 t1 (Tau t2) -> eqit RR true b2 t1 t2. -Proof. - intros. punfold H. red in H. simpl in *. - remember (TauF t2) as tt2. genobs t1 ot1. - hinduction H before b2; intros; try discriminate. - - inv Heqtt2. pclearbot. pstep. red. simpobs. econstructor; eauto. pstep_reverse. - - red in IHeqitF. pstep. red; simpobs. econstructor; eauto. pstep_reverse. - - inv Heqtt2. punfold_reverse H. -Qed. - -Lemma eqit_inv_tauLR {E R1 R2 RR} b1 b2 t1 t2 : - @eqit E R1 R2 RR b1 b2 (Tau t1) (Tau t2) -> eqit RR b1 b2 t1 t2. -Proof. - intros. punfold H. red in H. simpl in *. - remember (TauF t1) as tt1. remember (TauF t2) as tt2. - hinduction H before b2; intros; try discriminate. - - inv Heqtt1. inv Heqtt2. pclearbot. eauto. - - inv Heqtt1. inv H; eauto. - + pclearbot. punfold REL. pstep. red. simpobs. eauto. - + pstep. red. simpobs. econstructor; eauto. pstep_reverse. apply IHeqitF; eauto. - - inv Heqtt2. inv H; eauto. - + pclearbot. punfold REL. pstep. red. simpobs. eauto. - + pstep. red. simpobs. econstructor; eauto. pstep_reverse. apply IHeqitF; eauto. + eqit b1 b2 RR (Vis e1 k1) (Vis e2 k2) -> e1 = e2 /\ (forall u, eqit b1 b2 RR (k1 u) (k2 u)). +Proof. + intros. destruct H as [? H]. + assert (WFo := wfo_wf _ o). induction WFo. + punfold H. repeat red in H. simpl in H. + dependent destruction H. + - split; eauto. intros y. destruct (REL y). pclearbot. eauto. + - eapply H1; eauto. + pclearbot. rewrite <-x1, <-x. punfold REL. +Qed. + +Lemma eqiti_inv_tauL E b1 R1 R2 RR o o' t1 t2 + (REL: @eqiti E b1 true R1 R2 RR o (Tau t1) t2) + (LT: wfo_lt o o') + : eqiti b1 true RR o' t1 t2. +Proof. + revert_until RR. pcofix CIH. intros. + revert_until o. assert (WF := wfo_wf _ o). induction WF; intros. + pfold. punfold REL. red in REL |- *. inv REL. + - econstructor; eauto. + pclearbot. left. eapply paco6_mon_bot; eauto. + eapply eqiti_mon; eauto. + - pclearbot. punfold REL0. + eapply eqitF_mono; eauto using wfo_lt_le, wfo_le_le_le, upaco6_mon_bot. + - econstructor; eauto. + right. eapply CIH; eauto. + pclearbot. punfold REL0. pfold. rewrite <- H2. eauto. + - econstructor; eauto. + right. eapply CIH; eauto. + pclearbot. punfold REL0. pfold. rewrite <- H2. eauto. +Qed. + +Lemma eqiti_inv_tauR E b2 R1 R2 RR o o' t1 t2 + (REL: @eqiti E true b2 R1 R2 RR o t1 (Tau t2)) + (LT: wfo_lt o o') + : eqiti true b2 RR o' t1 t2. +Proof. + revert_until RR. pcofix CIH. intros. + revert_until o. assert (WF := wfo_wf _ o). induction WF; intros. + pfold. punfold REL. red in REL |- *. inv REL. + - econstructor; eauto. + pclearbot. left. eapply paco6_mon_bot; eauto. + eapply eqiti_mon; eauto. + - econstructor; eauto. + right. eapply CIH; eauto. + pclearbot. punfold REL0. pfold. rewrite <- H3. eauto. + - pclearbot. punfold REL0. + eapply eqitF_mono; eauto using wfo_lt_le, wfo_le_le_le, upaco6_mon_bot. + - econstructor; eauto. + right. eapply CIH; eauto. + pclearbot. punfold REL0. pfold. rewrite <- H3. eauto. +Qed. + +Lemma eqiti_inv_tauLR E b1 b2 R1 R2 RR o t1 t2 + (REL: @eqiti E b1 b2 R1 R2 RR o (Tau t1) (Tau t2)) + : eqiti b1 b2 RR o t1 t2. +Proof. + revert_until o. assert (WF := wfo_wf _ o). induction WF as [o _ HYP]; intros. + punfold REL. red in REL. inv REL; pclearbot; subst. + - eauto using eqiti_mon. + - destruct b1; inv CHECK. + eapply eqiti_inv_tauR; eauto. + punfold REL0. pfold. red. rewrite <-H. eauto. + - destruct b2; inv CHECK. + eapply eqiti_inv_tauL; eauto. + punfold REL0. pfold. red. rewrite <-H0. eauto. + - pstep. econstructor; eauto. + left. eapply HYP; eauto. + rewrite <-H,<-H0. pstep. punfold REL0. Qed. Lemma eqit_inv_ret_vis: forall {E X R1 R2 RR} b1 b2 (r: R1) (e: E X) k, - @eqit E R1 R2 RR b1 b2 (Ret r) (Vis e k) -> False. + @eqit E b1 b2 R1 R2 RR (Ret r) (Vis e k) -> False. Proof. - intros. + intros. destruct H as [? H]. + assert (WF := wfo_wf _ o). induction WF as [o _ HYP]; intros. punfold H; inv H. + eapply HYP; eauto. + rewrite <-H1, <-H2. pclearbot. pstep. punfold REL. Qed. Lemma eutt_inv_ret_vis: forall {X Y E} (x: X) (e: E Y) k, Ret x ≈ Vis e k -> False. Proof. - intros; eapply eqit_inv_ret_vis; eauto. + intros. destruct H. eapply eqit_inv_ret_vis; eauto. Qed. Lemma eqitree_inv_ret_vis: forall {X Y E} (x: X) (e: E Y) k, Ret x ≅ Vis e k -> False. Proof. - intros; eapply eqit_inv_ret_vis; eauto. + intros. destruct H. eapply eqit_inv_ret_vis; eauto. Qed. Lemma eqit_inv_tau_vis: forall {E X R1 R2 RR} b2 (e: E X) k t, - @eqit E R1 R2 RR false b2 (Tau t) (Vis e k) -> False. + @eqit E false b2 R1 R2 RR (Tau t) (Vis e k) -> False. Proof. - intros. + intros. destruct H as [? H]. punfold H; inv H. - inv CHECK. + inv CHECK. inv CHECK1. Qed. Lemma eqit_inv_vis_tau: forall {E X R1 R2 RR} b1 (e: E X) k t, - @eqit E R1 R2 RR b1 false (Vis e k) (Tau t) -> False. + @eqit E b1 false R1 R2 RR (Vis e k) (Tau t) -> False. Proof. - intros. + intros. destruct H as [? H]. punfold H; inv H. - inv CHECK. + inv CHECK. inv CHECK2. Qed. Lemma euttge_inv_tau_vis: forall {E A B} (e: E A) (k : A -> itree E B) (a : itree E B), Vis e k ≳ Tau a -> False. Proof. - intros; eapply eqit_inv_vis_tau; eauto. + intros. destruct H. eapply eqit_inv_vis_tau; eauto. Qed. Lemma eqitree_inv_tau_vis: forall {E A B} (e: E A) (k : A -> itree E B) (a : itree E B), Tau a ≅ Vis e k -> False. Proof. - intros; eapply eqit_inv_tau_vis; eauto. + intros. destruct H. eapply eqit_inv_tau_vis; eauto. Qed. Lemma eqit_inv_ret_tau: forall {E R1 R2 RR} b1 (r: R1) t, - @eqit E R1 R2 RR b1 false (Ret r) (Tau t) -> False. + @eqit E b1 false R1 R2 RR (Ret r) (Tau t) -> False. Proof. - intros. + intros. destruct H as [? H]. punfold H; inv H. - inv CHECK. + inv CHECK. inv CHECK2. Qed. Lemma eqit_inv_tau_ret: forall {E R1 R2 RR} b2 (r: R2) t, - @eqit E R1 R2 RR false b2 (Tau t) (Ret r) -> False. + @eqit E false b2 R1 R2 RR (Tau t) (Ret r) -> False. Proof. - intros. + intros. destruct H as [? H]. punfold H; inv H. - inv CHECK. + inv CHECK. inv CHECK1. Qed. Lemma euttge_inv_ret_tau: forall {E A} (r : A) (a : itree E A), Ret r ≳ Tau a -> False. Proof. - intros; eapply eqit_inv_ret_tau; eauto. + intros. destruct H. eapply eqit_inv_ret_tau; eauto. Qed. Lemma eqitree_inv_ret_tau: forall {E A} (r : A) (a : itree E A), Ret r ≅ Tau a -> False. Proof. - intros; eapply eqit_inv_ret_tau; eauto. + intros. destruct H. eapply eqit_inv_ret_tau; eauto. Qed. Lemma eutt_inv_ret {E R} r1 r2 : (Ret r1: itree E R) ≈ (Ret r2) -> r1 = r2. Proof. - intros; eapply eqit_inv_ret; eauto. + intros. destruct H. eapply eqit_inv_ret; eauto. Qed. Lemma eqitree_inv_ret {E R} r1 r2 : (Ret r1: itree E R) ≅ (Ret r2) -> r1 = r2. Proof. - intros; eapply eqit_inv_ret; eauto. + intros. destruct H. eapply eqit_inv_ret; eauto. Qed. +(** [eqit] is a congruence for [itree] constructors. *) + Lemma eqit_tauL {E R1 R2 RR} b2 (t1 : itree E R1) (t2 : itree E R2) : - eqit RR true b2 t1 t2 -> eqit RR true b2 (Tau t1) t2. + eqit true b2 RR t1 t2 -> eqit true b2 RR (Tau t1) t2. Proof. - intros. pstep. econstructor; eauto. punfold H. + intros. destruct H as [? H]. eexists. pstep. econstructor; eauto using wfo_add_one. Qed. Lemma eqit_tauR {E R1 R2 RR} b1 (t1 : itree E R1) (t2 : itree E R2) : - eqit RR b1 true t1 t2 -> eqit RR b1 true t1 (Tau t2). + eqit b1 true RR t1 t2 -> eqit b1 true RR t1 (Tau t2). +Proof. + intros. destruct H as [? H]. eexists. pstep. econstructor; eauto using wfo_add_one. +Qed. + +Lemma eqit_tau {E R1 R2 RR} b1 b2 (t1 : itree E R1) (t2 : itree E R2) : + eqit b1 b2 RR (Tau t1) (Tau t2) <-> eqit b1 b2 RR t1 t2. Proof. - intros. pstep. econstructor; eauto. punfold H. + split; intros []. + - eexists. eapply eqiti_inv_tauLR. eauto. + - eexists. pstep. econstructor; eauto using wfo_le_refl. +Qed. + +Lemma eqit_vis {E R1 R2 RR} b1 b2 {U} (e : E U) + (k1 : U -> itree E R1) (k2 : U -> itree E R2) : + (forall u, eqit b1 b2 RR (k1 u) (k2 u)) + <-> eqit b1 b2 RR (Vis e k1) (Vis e k2). +Proof. + split; intros. + - exists wfo_zero. pstep. econstructor. intros. destruct (H v). eauto. + - eapply eqit_inv_vis; eauto. +Qed. + +Lemma eqit_ret {E R1 R2 RR} b1 b2 (r1 : R1) (r2 : R2) : + RR r1 r2 <-> @eqit E b1 b2 _ _ RR (Ret r1) (Ret r2). +Proof. + split; intros H. + - exists wfo_zero. pstep. constructor; auto. + - eapply eqit_inv_ret; eauto. Qed. Lemma tau_euttge {E R} (t: itree E R) : @@ -727,87 +832,628 @@ Qed. Lemma simpobs {E R} {ot} {t: itree E R} (EQ: ot = observe t): t ≅ go ot. Proof. - pstep. repeat red. simpobs. simpl. subst. pstep_reverse. apply Reflexive_eqit; eauto. + exists wfo_zero. pstep. + unfold_eqit. simpobs. simpl. subst. fold_eqit. + pstep_reverse. eapply Reflexive_eqiti; eauto. Qed. -(** *** Transitivity properties *) +(*************************) +(** *** Eqit Lower Order *) +(*************************) -Inductive rcompose {R1 R2 R3} (RR1: R1->R2->Prop) (RR2: R2->R3->Prop) (r1: R1) (r3: R3) : Prop := -| rcompose_intro r2 (REL1: RR1 r1 r2) (REL2: RR2 r2 r3) +Variant euttOrdF (euttOrd : Type) := +| OBaseF +| OTauF (o : euttOrd) +| OStepF (o : euttOrd) +. +Arguments OBaseF {euttOrd}. +Arguments OStepF {euttOrd} o. +Arguments OTauF {euttOrd} o. + +CoInductive euttOrd : Type := ord_go +{ ord_observe : euttOrdF euttOrd }. + +Notation euttOrd' := (euttOrdF euttOrd). +Notation OBase := {| ord_observe := OBaseF |}. +Notation OTau o := {| ord_observe := OTauF o |}. +Notation OStep o := {| ord_observe := OStepF o |}. + +Inductive euttOrd_le': euttOrd' -> euttOrd' -> Prop := +| euttOrd_le_refl + o + : euttOrd_le' o o +| euttOrd_le_step + o1 o2 + (REL: euttOrd_le' o1 (ord_observe o2)) + : euttOrd_le' o1 (OStepF o2) +| euttOrd_le_tau + o1 o2 + (REL: euttOrd_le' o1 (ord_observe o2)) + : euttOrd_le' o1 (OTauF o2) . -Hint Constructors rcompose: core. +Hint Constructors euttOrd_le'. + +Definition euttOrd_le o1 o2 := euttOrd_le' (ord_observe o1) (ord_observe o2). +Hint Unfold euttOrd_le. + +Inductive euttOrd_lt': euttOrd' -> euttOrd' -> Prop := +| euttOrd_lt_step + o1 o2 + (REL: euttOrd_le' o1 (ord_observe o2)) + : euttOrd_lt' o1 (OStepF o2) +| euttOrd_tau + o1 o2 + (REL: euttOrd_lt' o1 (ord_observe o2)) + : euttOrd_lt' o1 (OTauF o2) +. +Hint Constructors euttOrd_lt'. + +Definition euttOrd_lt o1 o2 := euttOrd_lt' (ord_observe o1) (ord_observe o2). +Hint Unfold euttOrd_lt. + +Lemma euttOrd_lt_le: forall i j, euttOrd_lt i j -> euttOrd_le i j. +Proof. + unfold euttOrd_le, euttOrd_lt. intros i j. + generalize (ord_observe i) as oi, (ord_observe j) as oj. + intros. induction H; eauto. +Qed. -Lemma trans_rcompose {R} RR (TRANS: Transitive RR): - forall x y : R, rcompose RR RR x y -> RR x y. +Lemma euttOrd_le_le_le: forall i j k, euttOrd_le i j -> euttOrd_le j k -> euttOrd_le i k. Proof. - intros. destruct H; eauto. + unfold euttOrd_le. intros i j k. + generalize (ord_observe i) as oi, (ord_observe j) as oj, (ord_observe k) as ok. + intros. revert ok H0. + induction H; eauto; intros. + - remember (OStepF o2) as o2' in *. induction H0; subst; eauto. + - remember (OTauF o2) as o2' in *. induction H0; subst; eauto. Qed. -Lemma eqit_trans {E R1 R2 R3} (RR1: R1->R2->Prop) (RR2: R2->R3->Prop) b1 b2 t1 t2 t3 - (INL: eqit RR1 b1 b2 t1 t2) - (INR: eqit RR2 b1 b2 t2 t3): - @eqit E _ _ (rcompose RR1 RR2) b1 b2 t1 t3. +Lemma euttOrd_lt_le_lt: forall i j k, euttOrd_lt i j -> euttOrd_le j k -> euttOrd_lt i k. +Proof. + unfold euttOrd_le, euttOrd_lt. intros i j k. + generalize (ord_observe i) as oi, (ord_observe j) as oj, (ord_observe k) as ok. + intros. revert ok H0. + induction H; eauto; intros. + - remember (OStepF o2) as o2' in *. induction H0; subst; eauto. + econstructor. eapply (euttOrd_lt_le (ord_go _)). eauto. + - remember (OTauF o2) as o2' in *. induction H0; subst; eauto. + econstructor. eapply (euttOrd_lt_le (ord_go _)). eauto. +Qed. + +Lemma euttOrd_le_lt_lt: forall i j k, euttOrd_le i j -> euttOrd_lt j k -> euttOrd_lt i k. +Proof. + unfold euttOrd_le, euttOrd_lt. intros i j k. + generalize (ord_observe i) as oi, (ord_observe j) as oj, (ord_observe k) as ok. + intros. revert oi H. + induction H0; eauto; intros. + econstructor. eapply (euttOrd_le_le_le (ord_go _) (ord_go _)); eauto. +Qed. + +Program Definition euttOrdWf : bwfo := + {| bwfo_set := sig (Acc euttOrd_lt); + bwfo_le o1 o2 := euttOrd_le o1 o2; + bwfo_lt o1 o2 := euttOrd_lt o1 o2; + |}. +Next Obligation. eauto using euttOrd_lt_le. Qed. +Next Obligation. eauto using euttOrd_le_le_le. Qed. +Next Obligation. eauto using euttOrd_lt_le_lt. Qed. +Next Obligation. eauto using euttOrd_le_lt_lt. Qed. +Next Obligation. + red; intros. destruct a as [o WFo]. + generalize WFo. induction WFo as [o' _ HYP]. intros. + econstructor; intros. destruct y as [y WFy]. eauto. +Qed. + +CoFixpoint eutt_ord {E R1 R2} (ot1: itree' E R1) (ot2: itree' E R2) : euttOrd := + match ot1, ot2 with + | TauF t1', TauF t2' => OTau (eutt_ord (observe t1') (observe t2')) + | TauF t1', _ => OStep (eutt_ord (observe t1') ot2) + | _, TauF t2' => OStep (eutt_ord ot1 (observe t2')) + | _, _ => OBase + end. + +Lemma eutt_ord_wf {E b1 b2 R1 R2 RR o t1 t2} + (REL: @eqiti E b1 b2 R1 R2 RR o t1 t2): + Acc euttOrd_lt (eutt_ord (observe t1) (observe t2)). +Proof. + revert t1 t2 REL. assert (WF:= wfo_wf gwfo o). + induction WF as [o ACC HYP]. intros. + econstructor. intros. red in H. + remember (ord_observe y) as oy. + remember (ord_observe (eutt_ord (observe t1) (observe t2))) as ot. + revert t1 t2 REL y Heqoy Heqot. induction H; intros. + - punfold REL0. red in REL0. revert_until REL0. + inv REL0; intros; subst; try (inv Heqot; fail); pclearbot. + + assert (EQo2: o2 = eutt_ord (observe t0) (observe t3)). + { destruct (observe t3); inv Heqot; eauto. } + subst. econstructor. intros. eapply HYP; eauto using euttOrd_lt_le_lt. + + assert (EQo2: o2 = eutt_ord (observe t0) (observe t3)). + { destruct (observe t0); inv Heqot; eauto. } + subst. econstructor. intros. eapply HYP; eauto using euttOrd_lt_le_lt. + + econstructor; intros. + eapply (HYP _ LTo _ _ REL1). + eapply euttOrd_lt_le_lt; eauto. + eapply euttOrd_le_le_le; eauto. + red. rewrite <- Heqot. eauto. + - subst. genobs t1 ot1. genobs t2 ot2. + destruct ot1, ot2; inversion Heqot. + eapply IHeuttOrd_lt'; [| |rewrite <- H1]; eauto. + eapply eqiti_inv_tauLR. + punfold REL. pfold. red. rewrite Heqot1, Heqot2. eauto. +Qed. + +Lemma eqiti_lower_order {E b1 b2 R1 R2 RR o t1 t2} + (REL: @eqiti E b1 b2 R1 R2 RR o t1 t2): + exists so: euttOrdWf, eqiti b1 b2 RR (gwf_embed so) t1 t2. +Proof. + exists (exist _ (eutt_ord (observe t1) (observe t2)) (eutt_ord_wf REL)). + revert_until b2. pcofix CIH. intros. + generalize (eutt_ord_wf REL) as WF. + revert_until o. assert (WFo := wfo_wf _ o). induction WFo as [o _ HYP]. intros. + revert WF. punfold REL. pfold. red. inv REL; intros. + - eauto. + - econstructor. intros. specialize (REL0 v). destruct REL0. eauto. + - pclearbot. econstructor; eauto. + eapply gwf_embed_le_preserve. do 2 econstructor. + - genobs t3 ot3. destruct ot3. + + unfold_eta. eapply EqTauL; eauto. + eapply gwf_embed_lt_preserve. do 2 econstructor. + + econstructor. right. eapply CIH. + eapply gwf_embed_le_preserve. do 2 econstructor. + + unfold_eta. eapply EqTauL; eauto. + eapply gwf_embed_lt_preserve. do 2 econstructor. + - genobs t0 ot0. destruct ot0. + + unfold_eta. eapply EqTauR; eauto. + eapply gwf_embed_lt_preserve. do 2 econstructor. + + econstructor. right. eapply CIH. + eapply gwf_embed_le_preserve. do 2 econstructor. + + unfold_eta. eapply EqTauR; eauto. + eapply gwf_embed_lt_preserve. do 2 econstructor. + - pclearbot. hexploit HYP; eauto. intros EQIT. punfold EQIT. +Grab Existential Variables. + { pclearbot. simpl in *. rewrite Heqot0. punfold REL0. } + { pclearbot. punfold REL0. red in REL0. rewrite <-Heqot0 in REL0. + destruct b2; inversion CHECK. eauto using eqiti_inv_tauL. } + { pclearbot. simpl in *. rewrite Heqot0. punfold REL0. } + { pclearbot. simpl in *. rewrite Heqot3. punfold REL0. } + { pclearbot. punfold REL0. red in REL0. rewrite <-Heqot3 in REL0. + destruct b1; inversion CHECK. eauto using eqiti_inv_tauR. } + { pclearbot. simpl in *. rewrite Heqot3. punfold REL0. } + { pclearbot. eauto. } + { pclearbot. eauto. } +Qed. + +Lemma eqit_lower_order {E b1 b2 R1 R2 RR t1 t2} + (REL: @eqit E b1 b2 R1 R2 RR t1 t2): + exists so: euttOrdWf, eqiti b1 b2 RR (gwf_embed so) t1 t2. +Proof. destruct REL. eauto using eqiti_lower_order. Qed. + +Lemma euttOrd_small n (so: euttOrdWf) : + wfo_lt (gwf_embed so) (wfo_nat (S (S n))). +Proof. + econstructor. simpl. nia. +Qed. + +Lemma eq_itree_zero {E} b1 b2 R1 R2 RR t1 t2 + (REL: @eq_itree E R1 R2 RR t1 t2): + eqiti b1 b2 RR wfo_zero t1 t2. Proof. revert_until b2. pcofix CIH. intros. - pstep. punfold INL. punfold INR. red in INL, INR |- *. genobs_clear t3 ot3. - hinduction INL before CIH; intros; subst; clear t1 t2; eauto. - - remember (RetF r2) as ot. - hinduction INR before CIH; intros; inv Heqot; eauto with paco. - - assert (DEC: (exists m3, ot3 = TauF m3) \/ (forall m3, ot3 <> TauF m3)). - { destruct ot3; eauto; right; red; intros; inv H. } - destruct DEC as [EQ | EQ]. - + destruct EQ as [m3 ?]; subst. - econstructor. right. pclearbot. eapply CIH; eauto with paco. - eapply eqit_inv_tauLR. eauto. - + inv INR; try (exfalso; eapply EQ; eauto; fail). + destruct REL. punfold REL. pstep. red. + inv REL; try inv CHECK; try inv CHECK1; eauto. + - econstructor; eauto. + intros. destruct (REL0 v). pclearbot. + eexists. left. eapply paco6_mon_bot; [|eauto]. + eapply eqiti_mon; eauto with wfo_refl; destruct b1, b2; eauto. + - econstructor; eauto using wfo_non_negative. + pclearbot. right. eauto. +Qed. + +(********************************) +(** *** Eqit "Up-to" Principles *) +(********************************) + +(* Bind Closure *) + +Variant eqit_bind_rel {E} r s R1 R2 (RR:R1->R2->Prop) : + gwfo -> itree E R1 -> itree E R2 -> Prop := +| eqit_bind_split o o1 o2 U1 U2 (RU : U1 -> U2 -> Prop) t1 t2 k1 k2 + (EQV: r U1 U2 RU o1 t1 t2 : Prop) + (REL: forall u1 u2, RU u1 u2 -> s R1 R2 RR o2 (k1 u1) (k2 u2) : Prop) + (LEo: wfo_le (wfo_add o1 o2) o) +: eqit_bind_rel r s R1 R2 RR o (ITree.bind t1 k1) (ITree.bind t2 k2) +. +Hint Constructors eqit_bind_rel: core. +Arguments eqit_bind_split {E r s R1 R2 RR}. + +Definition eqit_bind_clo {E} r := @eqit_bind_rel E r r. +Hint Unfold eqit_bind_clo: core. + +Lemma eqit_bind_rel_monotone {E} r r' s s' R1 R2 RR o o' x y + (REL: @eqit_bind_rel E r s R1 R2 RR o x y) + (LEr: r <6= r') + (LEs: s <6= s') + (LEo: wfo_le o o') + : eqit_bind_rel r' s' R1 R2 RR o' x y. +Proof. + dependent destruction REL. + econstructor; eauto 7 using wfo_le_le_le. +Qed. + +Lemma eqit_bind_clo_prespectful {E} b1 b2: + prespectful6 (@eqit_ E b1 b2) eqit_bind_clo. +Proof. + econstructor; repeat intro. + - eapply eqit_bind_rel_monotone; eauto using wfo_le_refl. + - red in PR. eapply eqit_bind_rel_monotone in PR; [|apply GF|intros; apply PR0|eauto using wfo_le_refl]. + pstep. red. inversion PR; subst. + rewrite !unfold_bind_. inversion EQV. + + specialize (REL _ _ REL0). apply GF in REL. + eapply eqitF_mono; eauto using rclo6. + eapply wfo_le_le_le, LEo; apply wfo_add_proj_right. + + econstructor. intros. destruct (REL0 v). eauto 9 using wfo_le_refl. + + simpl. red in EQV. + econstructor; [eauto 8 using wfo_le_refl, rclo6|]. + eapply wfo_le_le_le; [|eauto]. + eapply wfo_add_le_left; eauto. + + rewrite <-unfold_bind_. econstructor; eauto 8 using wfo_le_refl. cycle 1. + eapply wfo_lt_le_lt; eauto. eapply wfo_add_lt_left; eauto. + + rewrite <-unfold_bind_. econstructor; eauto 8 using wfo_le_refl. + eapply wfo_lt_le_lt; eauto. eapply wfo_add_lt_left; eauto. + + rewrite <-!unfold_bind_. econstructor; eauto. + * right. right. econstructor; eauto using wfo_le_refl. + * eauto with wfo. +Qed. + +Lemma eqit_clo_bind E b1 b2: + @eqit_bind_clo E <7= gupaco6 (eqit_ b1 b2) (cpn6 (eqit_ b1 b2)). +Proof. + intros. eapply prespect6_uclo; eauto using eqit_bind_clo_prespectful with paco. +Qed. + +Arguments eqit_clo_bind : clear implicits. + +(* Transitivity Closure *) + +Inductive eqit_transL_clo {E} b b' + (r: forall R1 R2,(R1->R2->Prop)-> gwfo -> itree E R1 -> itree E R2 -> Prop) + R1 R2 (RR: R1->R2->Prop) o (t1: itree E R1) (t2: itree E R2) : Prop := +| eqit_transL_clo_intro o' o1 R1' R1R1' R1'R2 (t1': itree E R1') + (EQVl: @eqiti E b b' R1 R1' R1R1' o1 t1 t1') + (REL: r R1' R2 R1'R2 o' t1' t2 : Prop) + (LEo: wfo_le (wfo_add o' o1) o) + (LERR: forall t1 t2 t1', R1R1' t1 t1' -> R1'R2 t1' t2 -> RR t1 t2) + : eqit_transL_clo b b' r R1 R2 RR o t1 t2 +. +Hint Constructors eqit_transL_clo: core. + +Inductive eqit_transR_clo {E} b b' + (r: forall R1 R2,(R1->R2->Prop)-> gwfo -> itree E R1 -> itree E R2 -> Prop) + R1 R2 (RR: R1->R2->Prop) o (t1: itree E R1) (t2: itree E R2) : Prop := +| eqit_transR_clo_intro o' o2 R2' R2R2' R1R2' (t2': itree E R2') + (EQVr: @eqiti E b b' R2 R2' R2R2' o2 t2 t2') + (REL: r R1 R2' R1R2' o' t1 t2' : Prop) + (LERR2: forall t1 t2 t2', R2R2' t2 t2' -> R1R2' t1 t2' -> RR t1 t2) + (LEo: wfo_le (wfo_add o' o2) o) + : eqit_transR_clo b b' r R1 R2 RR o t1 t2 +. +Hint Constructors eqit_transR_clo: core. + +Lemma eqit_transL_clo_monotone {E} b b' r r' R1 R2 RR o o' x y + (REL: @eqit_transL_clo E b b' r R1 R2 RR o x y) + (LEr: r <6= r') + (LEo: wfo_le o o') + : eqit_transL_clo b b' r' R1 R2 RR o' x y. +Proof. + dependent destruction REL. + econstructor; eauto 7 using wfo_le_le_le. +Qed. + +Lemma eqit_transR_clo_monotone {E} b b' r r' R1 R2 RR o o' x y + (REL: @eqit_transR_clo E b b' r R1 R2 RR o x y) + (LEr: r <6= r') + (LEo: wfo_le o o') + : eqit_transR_clo b b' r' R1 R2 RR o' x y. +Proof. + dependent destruction REL. + econstructor; eauto 7 using wfo_le_le_le. +Qed. + +Lemma eqit_transL_clo_prespectful {E} bL bR: + prespectful6 (@eqit_ E bL bR) (@eqit_transL_clo E bL bR). +Proof. + econstructor. + { repeat intro; eapply eqit_transL_clo_monotone; eauto using wfo_le_refl. } + + intros ? ? ? ? R1 R2 RR o t1 t2 []. + eapply paco6_mon; [|intros; right; apply PR]. + assert (GFl := GF _ _ _ _ _ _ REL). + punfold EQVl. pstep. red in GFl, EQVl |- *. + + revert EQVl. inversion GFl; intros; subst. + + (* [Ret] t1' = Ret r1, t2 = Ret r2 *) + { inversion EQVl; subst; eauto; pclearbot. + (* [TauL] t1 = Tau t0 *) + { unfold_eta. eapply EqTauL; eauto; cycle 1. + { instantiate (1:= o'0). eauto with wfo wfo_proj. } + punfold REL1. red in REL1. rewrite H3 in REL1. left. pstep. red. + revert REL1. clear H2. revert t0. + assert (WF := wfo_wf _ o'0). induction WF as [ord _ HYP]. intros. + dependent destruction REL1. + - rewrite <-x. econstructor. eauto. + - rewrite <-x0. econstructor; eauto. left. pstep. + pclearbot. punfold REL1. red in REL1. rewrite x in REL1. + eapply HYP; eauto. eauto with wfo. + - econstructor; eauto. left. pstep. + pclearbot. punfold REL1. red in REL1. rewrite x, x0 in REL1. + eapply HYP; eauto. eauto with wfo. + } + (* [Stutter] t1 = t0 *) + { unfold_eta. eapply EqStutter; eauto; cycle 1. + { instantiate (1:= o'0). eauto with wfo wfo_proj. } + punfold REL1. red in REL1. rewrite H3 in REL1. left. pstep. red. + revert REL1. clear H2. revert t0. + assert (WF := wfo_wf _ o'0). induction WF as [ord _ HYP]. intros. + dependent destruction REL1. + - rewrite <-x. econstructor. eauto. + - rewrite <-x0. econstructor; eauto. left. pstep. + pclearbot. punfold REL1. red in REL1. rewrite x in REL1. + eapply HYP; eauto. eauto with wfo. + - econstructor; eauto. left. pstep. + pclearbot. punfold REL1. red in REL1. rewrite x, x0 in REL1. + eapply HYP; eauto. eauto with wfo. + } + } + + (* [Vis] t1' = Vis e k1, t2 = Vis e k2 *) + { dependent destruction EQVl; pclearbot. + (* [Vis] t1 = Vis e k0 *) + { rewrite <-x. eapply EqVis; intros. + destruct (REL0 v), (REL1 v); pclearbot. + eexists. right. econstructor; eauto with wfo_refl. + } + (* [TauL] t1 = Tau t0 *) + { rewrite <-x0. unfold_eta. econstructor; eauto; cycle 1. + { instantiate (1:= o'0). eauto with wfo wfo_proj. } + punfold REL1. red in REL1. rewrite x in REL1. left. pstep. red. + revert REL1. clear x0. revert t0. + assert (WF := wfo_wf _ o'0). induction WF as [ord _ HYP]. intros. + dependent destruction REL1. + - rewrite <-x. econstructor. intros. + destruct (REL0 v). destruct (REL1 v). pclearbot. + eexists (wfo_add _ _). + right. econstructor; eauto with wfo_refl. + - rewrite <-x1. econstructor; eauto. left. pstep. + pclearbot. punfold REL1. red in REL1. rewrite x in REL1. + eapply HYP; eauto. eauto with wfo. + - econstructor; eauto. left. pstep. + pclearbot. punfold REL1. red in REL1. rewrite x, x1 in REL1. + eapply HYP; eauto. eauto with wfo. + } + (* [Stutter] t1 = t0 *) + { rewrite <-x0. unfold_eta. econstructor; eauto; cycle 1. + { instantiate (1:= o'0). eauto with wfo wfo_proj. } + punfold REL1. red in REL1. rewrite x in REL1. left. pstep. red. + revert REL1. clear x0. revert t0. + assert (WF := wfo_wf _ o'0). induction WF as [ord _ HYP]. intros. + dependent destruction REL1. + - rewrite <-x. econstructor. intros. + destruct (REL0 v). destruct (REL1 v). pclearbot. + eexists (wfo_add _ _). + right. econstructor; eauto with wfo_refl. + - rewrite <-x1. econstructor; eauto. left. pstep. + pclearbot. punfold REL1. red in REL1. rewrite x in REL1. + eapply HYP; eauto. eauto with wfo. + - econstructor; eauto. left. pstep. + pclearbot. punfold REL1. red in REL1. rewrite x, x1 in REL1. + eapply HYP; eauto. eauto with wfo. + } + } + + (* [Tau] t1' = Tau m1, t2 = Tau m2 *) + { inversion EQVl; subst; eauto; pclearbot. + (* [Tau] t1 = Tau m0 *) + { econstructor; eauto 7 with wfo. + } + (* [TauL] t1 = Tau t0 *) + { destruct bL; inv CHECK. + hexploit eqiti_inv_tauR. + { pstep. rewrite <-H3. punfold REL1. } + { eauto. } + intros RELt0m1. + econstructor. + - right. econstructor; eauto with wfo_refl. + - eauto with wfo. + } + (* [TauR] t1 = Tau t0 *) + { econstructor; eauto. + - right. econstructor; eauto using wfo_le_refl. + - eauto 8 with wfo. + } + (* [Stutter] t1 = Tau t0 *) + { destruct bL, bR; inv CHECK1; inv CHECK2. + unfold_eta. eapply EqStutter; eauto with wfo. + punfold REL1. red in REL1. rewrite H3 in REL1. left. pstep. red. + remember (wfo_add o'1 o'0) as ord. clear H2. revert o'1 t0 LTo REL1 Heqord. + assert (WF := wfo_wf _ ord). induction WF as [ord _ HYP]. intros. + dependent destruction REL1; pclearbot. + - rewrite <-x. econstructor. + + right. econstructor; eauto with wfo_refl. + + subst. eauto with wfo. + - rewrite <-x0. econstructor. + right. econstructor; try apply REL0; eauto with wfo_refl. + + eapply eqiti_inv_tauR; eauto. + pstep. red. rewrite <-x. punfold REL1. + + subst. eauto with wfo_refl. + - rewrite <-x. econstructor; eauto. + + right. econstructor; eauto with wfo_refl. + + subst. eauto with wfo. + - rewrite <-x0. eapply EqStutter; eauto. + + left. pstep. punfold REL1. red in REL1. rewrite x in REL1. + eapply HYP; try apply REL1; subst; eauto; eauto with wfo. + + subst. eauto with wfo. + } + } + + (* [TauL] t1' = Tau t0, t2 = t3 *) + { inversion EQVl; subst; eauto; pclearbot. + (* [Tau] t1 = Tau m1 *) + { econstructor; eauto. + + right. econstructor; eauto with wfo_refl. + + eauto with wfo. + } + (* [TauL] t1 = Tau t4 *) + { destruct bL; inv CHECK. + hexploit eqiti_inv_tauR. + { pstep. rewrite <-H3. punfold REL1. } + { eauto. } + intros RELt0m1. econstructor; eauto. - pclearbot. punfold REL. red in REL. - hinduction REL0 before CIH; intros; try (exfalso; eapply EQ; eauto; fail). - * remember (RetF r1) as ot. - hinduction REL0 before CIH; intros; inv Heqot; eauto with paco. - * remember (VisF e k1) as ot. - hinduction REL0 before CIH; intros; dependent destruction Heqot; eauto with paco. - econstructor. intros. right. - destruct (REL v), (REL0 v); try contradiction. eauto. - * eapply IHREL0; eauto. pstep_reverse. - destruct b1; inv CHECK0. - apply eqit_inv_tauR. eauto. - - remember (VisF e k2) as ot. - hinduction INR before CIH; intros; dependent destruction Heqot; eauto. - econstructor. intros. - destruct (REL v), (REL0 v); try contradiction; eauto. - - remember (TauF t0) as ot. - hinduction INR before CIH; intros; dependent destruction Heqot; eauto. - eapply IHINL; eauto. pclearbot. punfold REL. + - right. econstructor; eauto with wfo_refl. + - eauto with wfo. + } + (* [TauR] t1 = t4 *) + { econstructor; eauto. + - right. econstructor; eauto using wfo_le_refl. + - eauto 8 with wfo. + } + (* [Stutter] t1 = t4 *) + { destruct bL, bR; inv CHECK1; inv CHECK2. + eapply EqStutter; eauto. + - right. econstructor; cycle 1; eauto with wfo_refl. + eapply eqiti_inv_tauR; eauto. + rewrite <-H3. pstep. punfold REL1. + - eauto with wfo. + } + } + + (* [TauR] t1' = t0, t2 = Tau t3 *) + { econstructor; eauto 7 with wfo wfo_refl. + } + + (* [Stutter] ... *) + { econstructor; eauto 7 with wfo wfo_refl. + } +Qed. + +Lemma eqit_transR_clo_prespectful {E} bL bR: + prespectful6 (@eqit_ E bL bR) (@eqit_transR_clo E bR bL). +Proof. + econstructor. + { repeat intro; eapply eqit_transR_clo_monotone; eauto using wfo_le_refl. } + + intros ? ? ? ? R1 R2 RR o t1 t2 CLO. + apply eqiti_r_flip. + eapply paco6_mon. + - eapply eqit_transL_clo_prespectful. + + instantiate (1:= eqit_rel_flip r). + instantiate (1:= eqit_rel_flip l). + unfold eqit_rel_flip. eauto. + + unfold eqit_rel_flip. intros. + apply GF in PR. eauto using eqitF_flip. + + destruct CLO. econstructor; eauto. + * instantiate (1:= flip R1R2'). eauto. + * eauto. + - unfold eqit_rel_flip. + intros. destruct PR; eauto. + right. destruct H. econstructor; eauto. +Qed. + +Lemma eqit_clo_transL E bL bR: + @eqit_transL_clo E bL bR <7= gupaco6 (eqit_ bL bR) (cpn6 (eqit_ bL bR)). +Proof. + intros. eapply prespect6_uclo; eauto using eqit_transL_clo_prespectful with paco. +Qed. + +Lemma eqit_clo_transR E bL bR: + @eqit_transR_clo E bR bL <7= gupaco6 (eqit_ bL bR) (cpn6 (eqit_ bL bR)). +Proof. + intros. eapply prespect6_uclo; eauto using eqit_transR_clo_prespectful with paco. +Qed. + +Arguments eqit_clo_transL : clear implicits. +Arguments eqit_clo_transR : clear implicits. + +(** *** Bind properties *) + +Lemma eutt_clo_bind {E U1 U2 UU R1 R2 RR} t1 t2 k1 k2 + (EQT: @eutt E U1 U2 UU t1 t2) + (EQK: forall u1 u2, UU u1 u2 -> @eutt E R1 R2 RR (k1 u1) (k2 u2)): + eutt RR (x <- t1;; k1 x) (x <- t2;; k2 x). +Proof. + intros. destruct (eqit_lower_order EQT) as [so EQTso]. + eexists. ginit. guclo eqit_clo_bind. + econstructor; eauto using wfo_le_refl with paco. + intros. destruct (eqit_lower_order (EQK _ _ H)) as [so' RELso']. + gfinal. right. + eapply eqiti_mon; eauto using wfo_lt_le, (euttOrd_small 0). +Qed. + +(** *** Transitivity properties *) + +Lemma eqiti_trans {E} b1 b2 {R1 R2 R3} (RR1: R1->R2->Prop) (RR2: R2->R3->Prop) (RR: R1->R3->Prop) o1 o2 o t1 t2 t3 + (INL: eqiti b1 b2 RR1 o1 t1 t2) + (INR: eqiti b1 b2 RR2 o2 t2 t3) + (LEo: wfo_le (wfo_add o1 o2) o) + (RRComp: forall x y z, RR1 x y -> RR2 y z -> RR x z) + : @eqiti E b1 b2 _ _ RR o t1 t3. +Proof. + ginit. + guclo eqit_clo_transR. econstructor. + - eapply eqiti_flip. instantiate (3:= flip RR2). eauto. + - gfinal. eauto. + - eauto. + - eauto. +Qed. + +Lemma eqit_trans {E} b1 b2 {R1 R2 R3} (RR1: R1->R2->Prop) (RR2: R2->R3->Prop) (RR: R1->R3->Prop) t1 t2 t3 + (INL: eqit b1 b2 RR1 t1 t2) + (INR: eqit b1 b2 RR2 t2 t3) + (RRComp: forall x y z, RR1 x y -> RR2 y z -> RR x z) + : @eqit E b1 b2 _ _ RR t1 t3. +Proof. + destruct INL, INR. eexists. + eapply eqiti_trans; eauto with wfo_refl. +Qed. + +Lemma eutt_trans {E} {R1 R2 R3} (RR1: R1->R2->Prop) (RR2: R2->R3->Prop) (RR: R1->R3->Prop) t1 t2 t3 + (INL: eutt RR1 t1 t2) + (INR: eutt RR2 t2 t3) + (RRComp: forall x y z, RR1 x y -> RR2 y z -> RR x z) + : @eutt E _ _ RR t1 t3. +Proof. + destruct INL, INR. eexists. + eapply eqiti_trans; eauto with wfo_refl. Qed. Global Instance Transitive_eqit {E : Type -> Type} {R: Type} (RR : R -> R -> Prop) (b1 b2: bool): - Transitive RR -> Transitive (@eqit E _ _ RR b1 b2). + Transitive RR -> Transitive (@eqit E b1 b2 _ _ RR). Proof. - red; intros. eapply eqit_mon, eqit_trans; eauto using (trans_rcompose RR). + red; intros. eapply eqit_mon; [eapply eqit_trans|..]; eauto. Qed. Global Instance Transitive_eqit_eq {E : Type -> Type} {R: Type} (b1 b2: bool): - Transitive (@eqit E R R eq b1 b2). + Transitive (@eqit E b1 b2 R R eq). Proof. apply Transitive_eqit. repeat intro; subst; eauto. Qed. Global Instance Equivalence_eqit {E : Type -> Type} {R: Type} (RR : R -> R -> Prop) (b: bool): - Equivalence RR -> Equivalence (@eqit E R R RR b b). + Equivalence RR -> Equivalence (@eqit E b b R R RR). Proof. constructor; try typeclasses eauto. Qed. Global Instance Equivalence_eqit_eq {E : Type -> Type} {R: Type} (b: bool): - Equivalence (@eqit E R R eq false false). + Equivalence (@eqit E false false R R eq). Proof. constructor; try typeclasses eauto. Qed. Global Instance Transitive_eutt {E R RR} : Transitive RR -> Transitive (@eutt E R R RR). Proof. - red; intros. eapply eqit_mon, eqit_trans; eauto using (trans_rcompose RR). + red; intros. eapply eqit_mon; [eapply eqit_trans|..]; eauto. Qed. Global Instance Equivalence_eutt {E R RR} : Equivalence RR -> Equivalence (@eutt E R R RR). @@ -815,24 +1461,25 @@ Proof. constructor; try typeclasses eauto. Qed. -Global Instance geuttgen_cong_eqit {E R1 R2 RR1 RR2 RS} b1 b2 r rg +Global Instance geuttgen_cong_eqit {E R1 R2 RR1 RR2 RS} b1 b2 r rg o (LERR1: forall x x' y, (RR1 x x': Prop) -> (RS x' y: Prop) -> RS x y) (LERR2: forall x y y', (RR2 y y': Prop) -> RS x y' -> RS x y): Proper (eq_itree RR1 ==> eq_itree RR2 ==> flip impl) - (gpaco2 (@eqit_ E R1 R2 RS b1 b2 id) (eqitC RS b1 b2) r rg). + (gpaco6 (@eqit_ E b1 b2) (cpn6 (eqit_ b1 b2)) r rg R1 R2 RS o). Proof. - repeat intro. guclo eqit_clo_trans. econstructor; cycle -3; eauto. - - eapply eqit_mon, H; eauto; discriminate. - - eapply eqit_mon, H0; eauto; discriminate. + repeat intro. + guclo eqit_clo_transL. econstructor; eauto using eq_itree_zero, wfo_add_zero_r_le. + guclo eqit_clo_transR. econstructor; eauto using eq_itree_zero, wfo_add_zero_r_le. Qed. -Global Instance geuttgen_cong_eqit_eq {E R1 R2 RS} b1 b2 r rg: +Global Instance geuttgen_cong_eqit_eq {E R1 R2 RS} b1 b2 r rg o: Proper (eq_itree eq ==> eq_itree eq ==> flip impl) - (gpaco2 (@eqit_ E R1 R2 RS b1 b2 id) (eqitC RS b1 b2) r rg). + (gpaco6 (@eqit_ E b1 b2) (cpn6 (eqit_ b1 b2)) r rg R1 R2 RS o). Proof. eapply geuttgen_cong_eqit; intros; subst; eauto. Qed. +(* Global Instance geuttge_cong_euttge {E R1 R2 RR1 RR2 RS} r rg (LERR1: forall x x' y, (RR1 x x': Prop) -> (RS x' y: Prop) -> RS x y) (LERR2: forall x y y', (RR2 y y': Prop) -> RS x y' -> RS x y): @@ -860,38 +1507,41 @@ Qed. Global Instance geutt_cong_euttge_eq {E R1 R2 RS} r rg: Proper (euttge eq ==> euttge eq ==> flip impl) - (gpaco2 (@eqit_ E R1 R2 RS true true id) (eqitC RS true true) r rg). + (gpaco2 (@eqit_ E true true R1 R2 RS id) (eqitC RS true true) r rg). Proof. eapply geutt_cong_euttge; intros; subst; eauto. Qed. +*) Global Instance eqitgen_cong_eqit {E R1 R2 RR1 RR2 RS} b1 b2 (LERR1: forall x x' y, (RR1 x x': Prop) -> (RS x' y: Prop) -> RS x y) (LERR2: forall x y y', (RR2 y y': Prop) -> RS x y' -> RS x y): Proper (eq_itree RR1 ==> eq_itree RR2 ==> flip impl) - (@eqit E R1 R2 RS b1 b2). + (@eqit E b1 b2 R1 R2 RS). Proof. - ginit. intros. eapply geuttgen_cong_eqit; eauto. gfinal. eauto. + repeat intro. destruct H1. eexists. + ginit. eapply geuttgen_cong_eqit; eauto. gfinal. eauto. Qed. Global Instance eqitgen_cong_eqit_eq {E R1 R2 RS} b1 b2: Proper (eq_itree eq ==> eq_itree eq ==> flip impl) (@eqit E R1 R2 RS b1 b2). Proof. - ginit. intros. rewrite H1, H0. gfinal. eauto. + repeat intro. destruct H1. eexists. + ginit. intros. rewrite H, H0. gfinal. eauto. Qed. Global Instance euttge_cong_euttge {E R RS} (TRANS: Transitive RS): Proper (euttge RS ==> flip (euttge RS) ==> flip impl) - (@eqit E R R RS true false). + (@eqit E true false R R RS). Proof. - repeat intro. do 2 (eapply eqit_mon, eqit_trans; eauto using (trans_rcompose RS)). + repeat intro. do 2 (eapply eqit_mon; [eapply eqit_trans|..]; eauto). Qed. Global Instance euttge_cong_euttge_eq {E R}: Proper (euttge eq ==> flip (euttge eq) ==> flip impl) - (@eqit E R R eq true false). + (@eqit E true false R R eq). Proof. eapply euttge_cong_euttge; eauto using eq_trans. Qed. @@ -922,10 +1572,11 @@ Lemma bind_trigger {E R} U (e : E U) (k : U -> itree E R) : ITree.bind (ITree.trigger e) k ≅ Vis e (fun x => k x). Proof. rewrite unfold_bind; cbn. - pstep. + eexists. ginit. gstep. constructor. - intros; red. left. rewrite bind_ret_l. - apply Reflexive_eqit; eauto. + intros; eexists. rewrite bind_ret_l. + gfinal. right. eapply Reflexive_eqiti; eauto. +Grab Existential Variables. exact wfo_zero. exact wfo_zero. Qed. Lemma unfold_iter {E A B} (f : A -> itree E (A + B)) (x : A) : @@ -941,119 +1592,47 @@ Proof. reflexivity. Qed. -Ltac auto_ctrans := - intros; repeat (match goal with [H: rcompose _ _ _ _ |- _] => destruct H end); subst; eauto. -Ltac auto_ctrans_eq := try instantiate (1:=eq); auto_ctrans. - -Section eqit_h. - -Context {E : Type -> Type} {R1 R2 : Type} (RR : R1 -> R2 -> Prop). +(* Ltac auto_ctrans := *) +(* intros; repeat (match goal with [H: rcompose _ _ _ _ |- _] => destruct H end); subst; eauto. *) +(* Ltac auto_ctrans_eq := try instantiate (1:=eq); auto_ctrans. *) (** [eqit] is a congruence for [itree] constructors. *) -Lemma eqit_Tau b1 b2 (t1 : itree E R1) (t2 : itree E R2) : - eqit RR b1 b2 (Tau t1) (Tau t2) <-> eqit RR b1 b2 t1 t2. -Proof. - split; intros H. - - punfold H. red in H. simpl in *. pstep. red. - remember (TauF t1) as ot1. remember (TauF t2) as ot2. - hinduction H before RR; intros; subst; try inv Heqot1; try inv Heqot2; eauto. - + pclearbot. punfold REL. - + inv H; eauto. - + inv H; eauto. - - pstep. constructor; auto. -Qed. - -Lemma eqit_Vis b1 b2 {U} (e : E U) - (k1 : U -> itree E R1) (k2 : U -> itree E R2) : - (forall u, eqit RR b1 b2 (k1 u) (k2 u)) - <-> eqit RR b1 b2 (Vis e k1) (Vis e k2). -Proof. - split; intros H. - - pstep. econstructor. left. apply H. - - punfold H. inv H; auto_inj_pair2; subst; auto. - intros. pclearbot. eauto. -Qed. - -Lemma eqit_Ret b1 b2 (r1 : R1) (r2 : R2) : - RR r1 r2 <-> @eqit E _ _ RR b1 b2 (Ret r1) (Ret r2). -Proof. - split; intros H. - - pstep. constructor; auto. - - punfold H. inversion H; auto_inj_pair2; subst; auto. -Qed. - -(** *** "Up-to" principles for coinduction. *) - -Inductive eqit_bind_clo b1 b2 (r : itree E R1 -> itree E R2 -> Prop) : - itree E R1 -> itree E R2 -> Prop := -| pbc_intro_h U1 U2 (RU : U1 -> U2 -> Prop) t1 t2 k1 k2 - (EQV: eqit RU b1 b2 t1 t2) - (REL: forall u1 u2, RU u1 u2 -> r (k1 u1) (k2 u2)) - : eqit_bind_clo b1 b2 r (ITree.bind t1 k1) (ITree.bind t2 k2) -. -Hint Constructors eqit_bind_clo: core. - -Lemma eqit_clo_bind b1 b2 vclo - (MON: monotone2 vclo) - (CMP: compose (eqitC RR b1 b2) vclo <3= compose vclo (eqitC RR b1 b2)) - (ID: id <3= vclo): - eqit_bind_clo b1 b2 <3= gupaco2 (eqit_ RR b1 b2 vclo) (eqitC RR b1 b2). -Proof. - gcofix CIH. intros. destruct PR. - guclo eqit_clo_trans. - econstructor; auto_ctrans_eq; try (rewrite (itree_eta (x <- _;; _ x)), unfold_bind; reflexivity). - punfold EQV. unfold_eqit. - hinduction EQV before CIH; intros; pclearbot. - - guclo eqit_clo_trans. - econstructor; auto_ctrans_eq; try (rewrite <- !itree_eta; reflexivity). - eauto with paco. - - gstep. econstructor. eauto with paco. - - gstep. econstructor. eauto 7 with paco. - - destruct b1; try discriminate. - guclo eqit_clo_trans. - econstructor; auto_ctrans_eq; cycle -1; eauto; try reflexivity. - eapply eqit_tauL. rewrite unfold_bind, <-itree_eta. reflexivity. - - destruct b2; try discriminate. - guclo eqit_clo_trans. econstructor; auto_ctrans_eq; cycle -1; eauto; try reflexivity. - eapply eqit_tauL. rewrite unfold_bind, <-itree_eta. reflexivity. -Qed. - -Lemma eutt_clo_bind {U1 U2 UU} t1 t2 k1 k2 - (EQT: @eutt E U1 U2 UU t1 t2) - (EQK: forall u1 u2, UU u1 u2 -> eutt RR (k1 u1) (k2 u2)): - eutt RR (x <- t1;; k1 x) (x <- t2;; k2 x). -Proof. - intros. ginit. guclo eqit_clo_bind. - econstructor; eauto. intros; subst. gfinal. right. apply EQK. eauto. -Qed. - -End eqit_h. - Lemma eutt_Tau {E R} (t1 t2 : itree E R): Tau t1 ≈ Tau t2 <-> t1 ≈ t2. Proof. - apply eqit_Tau. + apply eqit_tau. Qed. Lemma eqitree_Tau {E R} (t1 t2 : itree E R): Tau t1 ≅ Tau t2 <-> t1 ≅ t2. Proof. - apply eqit_Tau. + apply eqit_tau. Qed. -Arguments eqit_clo_bind : clear implicits. -Hint Constructors eqit_bind_clo: core. +(* Specialization of [eutt_clo_bind] to the recurrent case where [UU := eq] + in order to avoid having to provide the relation manually everytime *) +Lemma eutt_eq_bind : forall E R U (t: itree E U) (k1 k2: U -> itree E R), (forall u, k1 u ≈ k2 u) -> ITree.bind t k1 ≈ ITree.bind t k2. +Proof. + intros. eapply eutt_clo_bind; [reflexivity|]. + intros; subst. eauto. +Qed. Lemma eqit_bind' {E R1 R2 S1 S2} (RR : R1 -> R2 -> Prop) b1 b2 (RS : S1 -> S2 -> Prop) t1 t2 k1 k2 : - eqit RR b1 b2 t1 t2 -> - (forall r1 r2, RR r1 r2 -> eqit RS b1 b2 (k1 r1) (k2 r2)) -> - @eqit E _ _ RS b1 b2 (ITree.bind t1 k1) (ITree.bind t2 k2). + eqit b1 b2 RR t1 t2 -> + (forall r1 r2, RR r1 r2 -> eqit b1 b2 RS (k1 r1) (k2 r2)) -> + @eqit E b1 b2 _ _ RS (ITree.bind t1 k1) (ITree.bind t2 k2). Proof. - intros. ginit. guclo eqit_clo_bind. unfold eqit in *. - econstructor; eauto with paco. + intros. eexists. + ginit. guclo eqit_clo_bind. + eapply eqit_bind_split; intros; eauto with wfo_refl. + - gfinal. right. destruct (eqit_lower_order H). + eapply eqiti_mon; eauto using wfo_lt_le, euttOrd_small. + - gfinal. right. destruct (eqit_lower_order (H0 _ _ H1)). + eapply eqiti_mon; eauto using wfo_lt_le, euttOrd_small. +Grab Existential Variables. exact 0. exact 0. Qed. Lemma eq_itree_clo_bind {E : Type -> Type} {R1 R2 : Type} (RR : R1 -> R2 -> Prop) {U1 U2 UU} t1 t2 k1 k2 @@ -1065,40 +1644,43 @@ Proof. Qed. Global Instance eqit_bind {E R S} b1 b2 : - Proper (pointwise_relation _ (eqit eq b1 b2) ==> - eqit eq b1 b2 ==> - eqit eq b1 b2) (@ITree.bind' E R S). + Proper (pointwise_relation _ (eqit b1 b2 eq) ==> + eqit b1 b2 eq ==> + eqit b1 b2 eq) (@ITree.bind' E R S). Proof. repeat intro; eapply eqit_bind'; eauto. intros; subst; auto. Qed. Global Instance eqit_bind_ {E R S} b1 b2 k : - Proper (going (eqit eq b1 b2) ==> - eqit eq b1 b2) (@ITree._bind E R S k (@ITree.bind' E R S k)). + Proper (going (eqit b1 b2 eq) ==> + eqit b1 b2 eq) (@ITree._bind E R S k (@ITree.bind' E R S k)). Proof. - ginit. intros. destruct H0. + eexists. ginit. destruct H. rewrite (itree_eta' x), (itree_eta' y), <- !unfold_bind. - guclo eqit_clo_bind. econstructor; eauto. - intros. subst. apply reflexivity. + guclo eqit_clo_bind. econstructor; eauto with wfo_refl; intros. + - gfinal. right. destruct (eqit_lower_order e). + eapply eqiti_mon; eauto using wfo_lt_le, euttOrd_small. + - subst. apply reflexivity. +Grab Existential Variables. exact 0. exact wfo_zero. Qed. Lemma eqit_map {E R1 R2 S1 S2} (RR : R1 -> R2 -> Prop) b1 b2 (RS : S1 -> S2 -> Prop) f1 f2 t1 t2 : (forall r1 r2, RR r1 r2 -> RS (f1 r1) (f2 r2)) -> - @eqit E _ _ RR b1 b2 t1 t2 -> - eqit RS b1 b2 (ITree.map f1 t1) (ITree.map f2 t2). + @eqit E b1 b2 _ _ RR t1 t2 -> + eqit b1 b2 RS (ITree.map f1 t1) (ITree.map f2 t2). Proof. unfold ITree.map; intros. eapply eqit_bind'; eauto. - intros; pstep; constructor; auto. + intros. eexists wfo_zero. pstep. econstructor. eauto. Qed. Global Instance eqit_eq_map {E R S} b1 b2 : Proper (pointwise_relation _ eq ==> - eqit eq b1 b2 ==> - eqit eq b1 b2) (@ITree.map E R S). + eqit b1 b2 eq ==> + eqit b1 b2 eq) (@ITree.map E R S). Proof. repeat intro; eapply eqit_map; eauto. intros; subst; auto. @@ -1108,9 +1690,10 @@ Lemma bind_ret_r {E R} : forall s : itree E R, ITree.bind s (fun x => Ret x) ≅ s. Proof. + eexists wfo_zero. revert R s. ginit. gcofix CIH. intros. rewrite !unfold_bind. gstep. repeat red. - genobs s os. destruct os; simpl; eauto with paco. + genobs s os. destruct os; simpl; eauto using wfo_non_negative with paco. Qed. Lemma bind_ret_r' {E R} (u : itree E R) (f : R -> R) : @@ -1118,10 +1701,12 @@ Lemma bind_ret_r' {E R} (u : itree E R) (f : R -> R) : (r <- u ;; Ret (f r)) ≅ u. Proof. intro H. rewrite <- (bind_ret_r u) at 2. apply eqit_bind. - - hnf. intros. apply eqit_Ret. auto. + - hnf. intros. apply eqit_ret. auto. - reflexivity. Qed. +(* ----------------- Revised Up Here ------------------ *) + Lemma bind_bind {E R S T} : forall (s : itree E R) (k : R -> itree E S) (h : S -> itree E T), ITree.bind (ITree.bind s k) h ≅ ITree.bind s (fun r => ITree.bind (k r) h). @@ -1230,7 +1815,7 @@ Proof. destruct (observe ma) eqn: Hobma. * exists r0. split. rewrite <- Hobma. tau_steps. reflexivity. cbn in *. rewrite <- H0. rewrite itree_eta, Hobtl. - apply eqit_Ret; auto. + apply eqit_ret; auto. * cbn in H0. rewrite itree_eta in H0. rewrite Hobtl in H0. apply eqitree_inv_ret_tau in H0. contradiction. * cbn in H0. rewrite itree_eta, Hobtl in H0. @@ -1300,7 +1885,7 @@ Proof. - intros. rewrite unfold_bind in H0. destruct (observe ma) eqn: Hobma; cbn in *; rewrite itree_eta in H0; rewrite <- Heqtl' in H0. + right. exists r. split. rewrite itree_eta. rewrite Hobma. reflexivity. - rewrite <- H0. apply eqit_Vis. + rewrite <- H0. apply eqit_vis. intros. destruct (REL u0); auto. inv H. + symmetry in H0. apply eqitree_inv_tau_vis in H0. contradiction. + setoid_rewrite itree_eta at 1. rewrite Hobma. clear Hobma Heqtl'. @@ -1389,7 +1974,7 @@ Proof. destruct (observe ma) eqn:Hobma. + cbn in *. right. exists r. rewrite itree_eta. rewrite Hobma. split; [reflexivity |]. - rewrite <- H0. apply eqit_Tau. pclearbot. auto. + rewrite <- H0. apply eqit_tau. pclearbot. auto. + cbn in *. left. exists t. rewrite itree_eta. rewrite Hobma. split; [reflexivity |]. rewrite eqitree_Tau in H0. rewrite <- H0. pclearbot. auto. @@ -1412,7 +1997,7 @@ Proof. * left. destruct H1 as (a & ? & ?). exists (Ret a). rewrite itree_eta. rewrite Hobma. rewrite H1. split; [reflexivity |]. rewrite unfold_bind. cbn. - apply eqit_tauL in H2. rewrite <- eqit_Tau. auto. + apply eqit_tauL in H2. rewrite <- eqit_tau. auto. + cbn in *. apply eqitree_inv_tau_vis in H0; contradiction. - intros. subst. inv Heqtr'. rewrite unfold_bind in H0. From 678f90689d17b88fd8914f5db5749f0e03d1a74e Mon Sep 17 00:00:00 2001 From: Gil Hur Date: Mon, 5 Oct 2020 15:56:09 +0900 Subject: [PATCH 2/3] Rename EqStutter to EqNone, OStep to OStutter --- theories/Eq/Eq.v | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/theories/Eq/Eq.v b/theories/Eq/Eq.v index 3c140b74..502c2bfa 100644 --- a/theories/Eq/Eq.v +++ b/theories/Eq/Eq.v @@ -137,7 +137,7 @@ Section eqit_Definition. (REL: sim o' t1 t2) (LTo: wfo_lt o' o) : eqitF b1 b2 RR sim o (observe t1) (TauF t2) - | EqStutter t1 t2 o' + | EqNone t1 t2 o' (CHECK1: b1) (CHECK2: b2) (REL: sim o' t1 t2) @@ -844,10 +844,10 @@ Qed. Variant euttOrdF (euttOrd : Type) := | OBaseF | OTauF (o : euttOrd) -| OStepF (o : euttOrd) +| OStutterF (o : euttOrd) . Arguments OBaseF {euttOrd}. -Arguments OStepF {euttOrd} o. +Arguments OStutterF {euttOrd} o. Arguments OTauF {euttOrd} o. CoInductive euttOrd : Type := ord_go @@ -856,7 +856,7 @@ CoInductive euttOrd : Type := ord_go Notation euttOrd' := (euttOrdF euttOrd). Notation OBase := {| ord_observe := OBaseF |}. Notation OTau o := {| ord_observe := OTauF o |}. -Notation OStep o := {| ord_observe := OStepF o |}. +Notation OStutter o := {| ord_observe := OStutterF o |}. Inductive euttOrd_le': euttOrd' -> euttOrd' -> Prop := | euttOrd_le_refl @@ -865,7 +865,7 @@ Inductive euttOrd_le': euttOrd' -> euttOrd' -> Prop := | euttOrd_le_step o1 o2 (REL: euttOrd_le' o1 (ord_observe o2)) - : euttOrd_le' o1 (OStepF o2) + : euttOrd_le' o1 (OStutterF o2) | euttOrd_le_tau o1 o2 (REL: euttOrd_le' o1 (ord_observe o2)) @@ -880,7 +880,7 @@ Inductive euttOrd_lt': euttOrd' -> euttOrd' -> Prop := | euttOrd_lt_step o1 o2 (REL: euttOrd_le' o1 (ord_observe o2)) - : euttOrd_lt' o1 (OStepF o2) + : euttOrd_lt' o1 (OStutterF o2) | euttOrd_tau o1 o2 (REL: euttOrd_lt' o1 (ord_observe o2)) @@ -904,7 +904,7 @@ Proof. generalize (ord_observe i) as oi, (ord_observe j) as oj, (ord_observe k) as ok. intros. revert ok H0. induction H; eauto; intros. - - remember (OStepF o2) as o2' in *. induction H0; subst; eauto. + - remember (OStutterF o2) as o2' in *. induction H0; subst; eauto. - remember (OTauF o2) as o2' in *. induction H0; subst; eauto. Qed. @@ -914,7 +914,7 @@ Proof. generalize (ord_observe i) as oi, (ord_observe j) as oj, (ord_observe k) as ok. intros. revert ok H0. induction H; eauto; intros. - - remember (OStepF o2) as o2' in *. induction H0; subst; eauto. + - remember (OStutterF o2) as o2' in *. induction H0; subst; eauto. econstructor. eapply (euttOrd_lt_le (ord_go _)). eauto. - remember (OTauF o2) as o2' in *. induction H0; subst; eauto. econstructor. eapply (euttOrd_lt_le (ord_go _)). eauto. @@ -947,8 +947,8 @@ Qed. CoFixpoint eutt_ord {E R1 R2} (ot1: itree' E R1) (ot2: itree' E R2) : euttOrd := match ot1, ot2 with | TauF t1', TauF t2' => OTau (eutt_ord (observe t1') (observe t2')) - | TauF t1', _ => OStep (eutt_ord (observe t1') ot2) - | _, TauF t2' => OStep (eutt_ord ot1 (observe t2')) + | TauF t1', _ => OStutter (eutt_ord (observe t1') ot2) + | _, TauF t2' => OStutter (eutt_ord ot1 (observe t2')) | _, _ => OBase end. @@ -1190,7 +1190,7 @@ Proof. eapply HYP; eauto. eauto with wfo. } (* [Stutter] t1 = t0 *) - { unfold_eta. eapply EqStutter; eauto; cycle 1. + { unfold_eta. eapply EqNone; eauto; cycle 1. { instantiate (1:= o'0). eauto with wfo wfo_proj. } punfold REL1. red in REL1. rewrite H3 in REL1. left. pstep. red. revert REL1. clear H2. revert t0. @@ -1273,7 +1273,7 @@ Proof. } (* [Stutter] t1 = Tau t0 *) { destruct bL, bR; inv CHECK1; inv CHECK2. - unfold_eta. eapply EqStutter; eauto with wfo. + unfold_eta. eapply EqNone; eauto with wfo. punfold REL1. red in REL1. rewrite H3 in REL1. left. pstep. red. remember (wfo_add o'1 o'0) as ord. clear H2. revert o'1 t0 LTo REL1 Heqord. assert (WF := wfo_wf _ ord). induction WF as [ord _ HYP]. intros. @@ -1289,7 +1289,7 @@ Proof. - rewrite <-x. econstructor; eauto. + right. econstructor; eauto with wfo_refl. + subst. eauto with wfo. - - rewrite <-x0. eapply EqStutter; eauto. + - rewrite <-x0. eapply EqNone; eauto. + left. pstep. punfold REL1. red in REL1. rewrite x in REL1. eapply HYP; try apply REL1; subst; eauto; eauto with wfo. + subst. eauto with wfo. @@ -1320,7 +1320,7 @@ Proof. } (* [Stutter] t1 = t4 *) { destruct bL, bR; inv CHECK1; inv CHECK2. - eapply EqStutter; eauto. + eapply EqNone; eauto. - right. econstructor; cycle 1; eauto with wfo_refl. eapply eqiti_inv_tauR; eauto. rewrite <-H3. pstep. punfold REL1. @@ -1705,7 +1705,7 @@ Proof. - reflexivity. Qed. -(* ----------------- Revised Up Here ------------------ *) +----------------- Revised Up Here ------------------ Lemma bind_bind {E R S T} : forall (s : itree E R) (k : R -> itree E S) (h : S -> itree E T), From 0d853c67396d3f1db90bb9a9556038e127404ae1 Mon Sep 17 00:00:00 2001 From: Gil Hur Date: Mon, 5 Oct 2020 19:28:41 +0900 Subject: [PATCH 3/3] Generalize gwfo into a lexicalgraphic order --- theories/Basics/GeneralWFO.v | 734 ++++++++++++++++++++--------------- theories/Eq/Eq.v | 4 +- 2 files changed, 423 insertions(+), 315 deletions(-) diff --git a/theories/Basics/GeneralWFO.v b/theories/Basics/GeneralWFO.v index 5ad9d79f..db32fac9 100644 --- a/theories/Basics/GeneralWFO.v +++ b/theories/Basics/GeneralWFO.v @@ -4,7 +4,7 @@ Require Import Arith Relations Max NPeano Program Wellfounded List Lia. From Paco Require Import paco. Import ListNotations. -Set Implicit Arguments. +Set Implicit Arguments. Global Set Bullet Behavior "Strict Subproofs". Ltac ginduction H := @@ -107,161 +107,359 @@ Structure bwfo := bwfo_le_le_le: forall i j k, bwfo_le i j -> bwfo_le j k -> bwfo_le i k; bwfo_lt_le_lt: forall i j k, bwfo_lt i j -> bwfo_le j k -> bwfo_lt i k; bwfo_le_lt_lt: forall i j k, bwfo_le i j -> bwfo_lt j k -> bwfo_lt i k; - + bwfo_wf : well_founded bwfo_lt; }. Arguments bwfo_lt {_} _ _. Arguments bwfo_le {_} _ _. +(** ** + Non-trival Non-negative Well-founded Ordered Monoids + *) + +Structure awfo := +{ wfo_set :> Type; + + wfo_zero : wfo_set; + wfo_add : wfo_set -> wfo_set -> wfo_set; + + wfo_lt : wfo_set -> wfo_set -> Prop; + wfo_le : wfo_set -> wfo_set -> Prop; + +(* Monoid *) + + wfo_add_zero_l_le: forall i, wfo_le (wfo_add wfo_zero i) i; + wfo_add_zero_l_ge: forall i, wfo_le i (wfo_add wfo_zero i); + wfo_add_zero_r_le: forall i, wfo_le (wfo_add i wfo_zero) i; + wfo_add_zero_r_ge: forall i, wfo_le i (wfo_add i wfo_zero); + + wfo_add_assoc_le: forall i j k, wfo_le (wfo_add i (wfo_add j k)) (wfo_add (wfo_add i j) k); + wfo_add_assoc_ge: forall i j k, wfo_le (wfo_add (wfo_add i j) k) (wfo_add i (wfo_add j k)); + +(* Order *) + + wfo_le_refl: forall i, wfo_le i i; + wfo_lt_le: forall i j, wfo_lt i j -> wfo_le i j; + wfo_le_le_le: forall i j k, wfo_le i j -> wfo_le j k -> wfo_le i k; + wfo_lt_le_lt: forall i j k, wfo_lt i j -> wfo_le j k -> wfo_lt i k; + wfo_le_lt_lt: forall i j k, wfo_le i j -> wfo_lt j k -> wfo_lt i k; + + wfo_add_le_left: forall i i' j (LE: wfo_le i i'), wfo_le (wfo_add i j) (wfo_add i' j); + wfo_add_le_right: forall i j j' (LE: wfo_le j j'), wfo_le (wfo_add i j) (wfo_add i j'); + wfo_add_lt_left: forall i i' j (LT: wfo_lt i i'), wfo_lt (wfo_add i j) (wfo_add i' j); + wfo_add_lt_right: forall i j j' (LT: wfo_lt j j'), wfo_lt (wfo_add i j) (wfo_add i j'); + +(* Well-founded *) + wfo_wf : well_founded wfo_lt; + +(* Positive *) + wfo_non_negative: forall i, wfo_le wfo_zero i; + +(* Non-trivial *) + wfo_one : wfo_set; + wfo_non_trivial : wfo_lt wfo_zero wfo_one; +}. + +Arguments wfo_lt {_} _ _. +Arguments wfo_le {_} _ _. +Arguments wfo_zero {_}. +Arguments wfo_one {_}. +Arguments wfo_add {_} _ _. + (* ** Symmetric Product of Algebraic Wellfounded Orders *) -Definition symprod_lt (a b : bwfo) (x y: a * b) := - (bwfo_lt (fst x) (fst y) /\ bwfo_le (snd x) (snd y)) \/ - (bwfo_le (fst x) (fst y) /\ bwfo_lt (snd x) (snd y)). +Definition symprod_lt (a b : awfo) (x y: a * b) := + (wfo_lt (fst x) (fst y) /\ wfo_le (snd x) (snd y)) \/ + (wfo_le (fst x) (fst y) /\ wfo_lt (snd x) (snd y)). -Definition symprod_le (a b : bwfo) (x y: a * b) := - bwfo_le (fst x) (fst y) /\ bwfo_le (snd x) (snd y). +Definition symprod_le (a b : awfo) (x y: a * b) := + wfo_le (fst x) (fst y) /\ wfo_le (snd x) (snd y). -Program Definition bwfo_symprod (a b : bwfo) : bwfo := - {| bwfo_lt := symprod_lt a b; - bwfo_le := symprod_le a b; +Program Definition awfo_symprod (a b : awfo) : awfo := + {| wfo_lt := symprod_lt a b; + wfo_le := symprod_le a b; + wfo_zero := (wfo_zero, wfo_zero); + wfo_one := (wfo_zero, wfo_one); + wfo_add := fun i j => (wfo_add (fst i) (fst j), wfo_add (snd i) (snd j)); |}. -Next Obligation. split; simpl; eauto using bwfo_le_refl. Qed. +Next Obligation. red. eauto using wfo_add_zero_l_le. Qed. +Next Obligation. red. eauto using wfo_add_zero_l_ge. Qed. +Next Obligation. red. eauto using wfo_add_zero_r_le. Qed. +Next Obligation. red. eauto using wfo_add_zero_r_ge. Qed. +Next Obligation. red. eauto using wfo_add_assoc_le. Qed. +Next Obligation. red. eauto using wfo_add_assoc_ge. Qed. +Next Obligation. split; simpl; eauto using wfo_le_refl. Qed. +Next Obligation. + destruct H as [[]|[]]; split; simpl in *; eauto using wfo_lt_le, wfo_le_le_le. +Qed. +Next Obligation. + destruct H, H0; split; simpl in *; eauto using wfo_le_le_le. +Qed. +Next Obligation. + destruct H, H, H0; [left|right]; split; simpl in *; eauto using wfo_lt_le_lt, wfo_le_le_le. +Qed. +Next Obligation. + destruct H, H0, H0; [left|right]; split; simpl in *; eauto using wfo_le_lt_lt, wfo_le_le_le. +Qed. Next Obligation. - destruct H as [[]|[]]; split; simpl in *; eauto using bwfo_lt_le, bwfo_le_le_le. + destruct LE; split; simpl in *; eauto using wfo_add_le_left. Qed. Next Obligation. - destruct H, H0; split; simpl in *; eauto using bwfo_le_le_le. + destruct LE; split; simpl in *; eauto using wfo_add_le_right. Qed. Next Obligation. - destruct H, H, H0; [left|right]; split; simpl in *; eauto using bwfo_lt_le_lt, bwfo_le_le_le. + destruct LT, H; [left|right]; split; simpl in *; eauto using wfo_add_lt_left, wfo_add_le_left. Qed. Next Obligation. - destruct H, H0, H0; [left|right]; split; simpl in *; eauto using bwfo_le_lt_lt, bwfo_le_le_le. + destruct LT, H; [left|right]; split; simpl in *; eauto using wfo_add_lt_right, wfo_add_le_right. Qed. Next Obligation. intros [u v]. - assert (WFu := bwfo_wf _ u). revert v. + assert (WFu := wfo_wf _ u). revert v. induction WFu as [u _ HYPu]. econstructor; intros [u' v'] LT'. destruct LT', H; simpl in *. - eapply HYPu in H; eauto. - clear v H0. - assert (WFv' := bwfo_wf _ v'). revert u' H. + assert (WFv' := wfo_wf _ v'). revert u' H. induction WFv' as [v' _ HYPv']. econstructor; intros [u'' v''] LT''. destruct LT'', H0; simpl in *. - + eapply HYPu; eauto using bwfo_lt_le_lt. - + eapply HYPv'; eauto using bwfo_le_le_le. + + eapply HYPu; eauto using wfo_lt_le_lt. + + eapply HYPv'; eauto using wfo_le_le_le. +Qed. +Next Obligation. split; simpl; eauto using wfo_non_negative. Qed. +Next Obligation. + right. simpl. split; eauto using wfo_non_trivial, wfo_le_refl. Qed. (* ** - Lexcographic Product of Algebraic Wellfounded Orders + Lexicographic Product of Algebraic Wellfounded Orders *) -Definition lexprod_lt (a b : bwfo) (x y: a * b) := - bwfo_lt (fst x) (fst y) \/ - (bwfo_le (fst x) (fst y) /\ bwfo_lt (snd x) (snd y)). +Definition lexprod_lt (a b : awfo) (x y: a * b) := + wfo_lt (fst x) (fst y) \/ + (wfo_le (fst x) (fst y) /\ wfo_lt (snd x) (snd y)). -Definition lexprod_le (a b : bwfo) (x y: a * b) := - bwfo_lt (fst x) (fst y) \/ - (bwfo_le (fst x) (fst y) /\ bwfo_le (snd x) (snd y)). +Definition lexprod_le (a b : awfo) (x y: a * b) := + wfo_lt (fst x) (fst y) \/ + (wfo_le (fst x) (fst y) /\ wfo_le (snd x) (snd y)). -Program Definition bwfo_lexprod (a b : bwfo) : bwfo := - {| bwfo_lt := lexprod_lt a b; - bwfo_le := lexprod_le a b; +Program Definition awfo_lexprod (a b : awfo) : awfo := + {| wfo_lt := lexprod_lt a b; + wfo_le := lexprod_le a b; + wfo_zero := (wfo_zero, wfo_zero); + wfo_one := (wfo_zero, wfo_one); + wfo_add := fun i j => (wfo_add (fst i) (fst j), wfo_add (snd i) (snd j)); |}. -Next Obligation. right. split; simpl; eauto using bwfo_le_refl. Qed. +Next Obligation. red. eauto using wfo_add_zero_l_le. Qed. +Next Obligation. red. eauto using wfo_add_zero_l_ge. Qed. +Next Obligation. red. eauto using wfo_add_zero_r_le. Qed. +Next Obligation. red. eauto using wfo_add_zero_r_ge. Qed. +Next Obligation. red. eauto using wfo_add_assoc_le. Qed. +Next Obligation. red. eauto using wfo_add_assoc_ge. Qed. +Next Obligation. right. split; simpl; eauto using wfo_le_refl. Qed. +Next Obligation. + destruct H as [|[]]; [left|right]; simpl in *; eauto using wfo_lt_le. +Qed. +Next Obligation. + destruct H as [|[]], H0 as [|[]]; [..|right]; try left; simpl in *; eauto using wfo_lt_le, wfo_lt_le_lt, wfo_le_lt_lt, wfo_le_le_le. +Qed. Next Obligation. - destruct H as [|[]]; [left|right]; simpl in *; eauto using bwfo_lt_le. + destruct H as [|[]], H0 as [|[]]; [..|right]; try left; simpl in *; eauto using wfo_lt_le, wfo_lt_le_lt, wfo_le_lt_lt, wfo_le_le_le. Qed. Next Obligation. - destruct H as [|[]], H0 as [|[]]; [..|right]; try left; simpl in *; eauto using bwfo_lt_le, bwfo_lt_le_lt, bwfo_le_lt_lt, bwfo_le_le_le. + destruct H as [|[]], H0 as [|[]]; [..|right]; try left; simpl in *; eauto using wfo_lt_le, wfo_lt_le_lt, wfo_le_lt_lt, wfo_le_le_le. Qed. Next Obligation. - destruct H as [|[]], H0 as [|[]]; [..|right]; try left; simpl in *; eauto using bwfo_lt_le, bwfo_lt_le_lt, bwfo_le_lt_lt, bwfo_le_le_le. + destruct LE as [|[]]; [left|right]; simpl in *; eauto using wfo_lt_le, wfo_lt_le_lt, wfo_le_lt_lt, wfo_le_le_le, wfo_add_lt_left, wfo_add_le_left. Qed. Next Obligation. - destruct H as [|[]], H0 as [|[]]; [..|right]; try left; simpl in *; eauto using bwfo_lt_le, bwfo_lt_le_lt, bwfo_le_lt_lt, bwfo_le_le_le. + destruct LE as [|[]]; [left|right]; simpl in *; eauto using wfo_lt_le, wfo_lt_le_lt, wfo_le_lt_lt, wfo_le_le_le, wfo_add_lt_right, wfo_add_le_right. +Qed. +Next Obligation. + destruct LT as [|[]]; [left|right]; simpl in *; eauto using wfo_lt_le, wfo_lt_le_lt, wfo_le_lt_lt, wfo_le_le_le, wfo_add_lt_left, wfo_add_le_left. +Qed. +Next Obligation. + destruct LT as [|[]]; [left|right]; simpl in *; eauto using wfo_lt_le, wfo_lt_le_lt, wfo_le_lt_lt, wfo_le_le_le, wfo_add_lt_right, wfo_add_le_right. Qed. Next Obligation. intros [u v]. - assert (WFu := bwfo_wf _ u). revert v. + assert (WFu := wfo_wf _ u). revert v. induction WFu as [u _ HYPu]. econstructor; intros [u' v'] LT'. destruct LT' as [|[]]; simpl in *. - eapply HYPu in H; eauto. - clear v H0. - assert (WFv' := bwfo_wf _ v'). revert u' H. + assert (WFv' := wfo_wf _ v'). revert u' H. induction WFv' as [v' _ HYPv']. econstructor; intros [u'' v''] LT''. destruct LT'' as [|[]]; simpl in *. - + eapply HYPu; eauto using bwfo_lt_le_lt. - + eapply HYPv'; eauto using bwfo_le_le_le. + + eapply HYPu; eauto using wfo_lt_le_lt. + + eapply HYPv'; eauto using wfo_le_le_le. +Qed. +Next Obligation. right. split; simpl; eauto using wfo_non_negative. Qed. +Next Obligation. + right. simpl. eauto using wfo_non_trivial, wfo_le_refl. Qed. -(** ** - Non-trival Non-negative Well-founded Ordered Monoids +(* ** + Simple Properties about Orders *) -Structure awfo := -{ wfo_set :> Type; +Lemma wfo_lt_neq: forall a i, ~ @wfo_lt a i i. +Proof. + intros. assert (WF := wfo_wf a i). red. + induction WF. eauto. +Qed. - wfo_zero : wfo_set; - wfo_add : wfo_set -> wfo_set -> wfo_set; +Lemma wfo_add_monotone: forall (a: awfo) (i i' j j': a) + (LEi: wfo_le i i') + (LEj: wfo_le j j'), + wfo_le (wfo_add i j) (wfo_add i' j'). +Proof. + eauto using wfo_le_le_le, wfo_add_le_left, wfo_add_le_right. +Qed. - wfo_lt : wfo_set -> wfo_set -> Prop; - wfo_le : wfo_set -> wfo_set -> Prop; +Lemma wfo_add_proj_left: forall a i j, @wfo_le a i (wfo_add i j). +Proof. + eauto using wfo_le_le_le, wfo_add_zero_r_ge, wfo_add_le_right, wfo_non_negative. +Qed. -(* Monoid *) - - wfo_add_zero_l_le: forall i, wfo_le (wfo_add wfo_zero i) i; - wfo_add_zero_l_ge: forall i, wfo_le i (wfo_add wfo_zero i); - wfo_add_zero_r_le: forall i, wfo_le (wfo_add i wfo_zero) i; - wfo_add_zero_r_ge: forall i, wfo_le i (wfo_add i wfo_zero); - - wfo_add_assoc_le: forall i j k, wfo_le (wfo_add i (wfo_add j k)) (wfo_add (wfo_add i j) k); - wfo_add_assoc_ge: forall i j k, wfo_le (wfo_add (wfo_add i j) k) (wfo_add i (wfo_add j k)); +Lemma wfo_add_proj_right: forall a i j, @wfo_le a j (wfo_add i j). +Proof. + eauto using wfo_le_le_le, wfo_add_zero_l_ge, wfo_add_le_left, wfo_non_negative. +Qed. -(* Order *) +Lemma wfo_add_one: forall (a: awfo) (i: a), wfo_lt i (wfo_add wfo_one i). +Proof. + eauto using wfo_le_lt_lt, wfo_add_proj_right, wfo_add_lt_left, wfo_non_trivial. +Qed. - wfo_le_refl: forall i, wfo_le i i; - wfo_lt_le: forall i j, wfo_lt i j -> wfo_le i j; - wfo_le_le_le: forall i j k, wfo_le i j -> wfo_le j k -> wfo_le i k; - wfo_lt_le_lt: forall i j k, wfo_lt i j -> wfo_le j k -> wfo_lt i k; - wfo_le_lt_lt: forall i j k, wfo_le i j -> wfo_lt j k -> wfo_lt i k; +(** [wfo_le_n n o o'] means that [o'] can be decreased at least [n] times + before reaching [o]. +*) +Inductive wfo_le_n {o: awfo} : nat -> o -> o -> Prop := +| wfo_le_n_Z i j (LE: wfo_le i j) + : wfo_le_n O i j +| wfo_le_n_S n i j k (GLE: wfo_le_n n i j) (LT: wfo_lt j k) + : wfo_le_n (S n) i k +. +Hint Constructors wfo_le_n. - wfo_add_le_left: forall i i' j (LE: wfo_le i i'), wfo_le (wfo_add i j) (wfo_add i' j); - wfo_add_le_right: forall i j j' (LE: wfo_le j j'), wfo_le (wfo_add i j) (wfo_add i j'); - wfo_add_lt_left: forall i i' j (LT: wfo_lt i i'), wfo_lt (wfo_add i j) (wfo_add i' j); - wfo_add_lt_right: forall i j j' (LT: wfo_lt j j'), wfo_lt (wfo_add i j) (wfo_add i j'); +Lemma wfo_le_n_lt: forall o n (i i': wfo_set o) + (LE: wfo_le_n (S n) i i'), + wfo_lt i i'. +Proof. + induction n; intros; inversion LE; subst. + - inversion GLE; subst. eauto using wfo_le_lt_lt. + - apply IHn in GLE. eauto using wfo_lt_le, wfo_lt_le_lt. +Qed. -(* Well-founded *) - wfo_wf : well_founded wfo_lt; +(* TODO rename (D) *) +Lemma wfo_le_n_S': forall o n (i i': wfo_set o) + (LE: wfo_le_n (S n) i i'), + exists j : wfo_set o, + wfo_lt i j /\ + wfo_le_n n j i'. +Proof. + induction n; intros; inversion LE; subst. + - inversion GLE. subst. eauto using wfo_le_lt_lt, wfo_le_refl. + - edestruct IHn; eauto. + destruct H. eauto. +Qed. -(* Positive *) - wfo_non_negative: forall i, wfo_le wfo_zero i; +Lemma wfo_le_n_S'': forall o n (i i': wfo_set o) + (LE: wfo_le_n (S n) i i'), + wfo_le_n n i i'. +Proof. + intros; inversion LE; inversion GLE; subst; eauto using wfo_lt_le, wfo_le_le_le, wfo_lt_le_lt. +Qed. -(* Non-trivial *) - wfo_one : wfo_set; - wfo_non_trivial : wfo_lt wfo_zero wfo_one; -}. +Lemma wfo_le_n_wfo_le: forall o n (i i' i'': wfo_set o) + (GLE: wfo_le_n n i i') + (LE: wfo_le i' i''), + wfo_le_n n i i''. +Proof. + intros; dependent destruction GLE; [econstructor 1|econstructor 2]; eauto using wfo_le_le_le, wfo_lt_le_lt. +Qed. + +Lemma wfo_le_n_anti: forall o m n (i i': wfo_set o) + (GLE: wfo_le_n m i i') + (LE: n <= m), + wfo_le_n n i i'. +Proof. + intros; ginduction LE; eauto. + intros; apply IHLE; auto using wfo_le_n_S''. +Qed. + +(* TODO rename *) +Lemma wfo_le_n_S_rev: forall o (i j: wfo_set o) n k + (LT: wfo_lt i j) + (GLE: wfo_le_n n j k), + wfo_le_n (S n) i k. +Proof. + intros; ginduction GLE; intros; eauto. + econstructor; eauto using wfo_lt_le_lt, wfo_le_refl. +Qed. + +Lemma wfo_le_n_plus: forall o n na nb (i i': wfo_set o) + (GLE: wfo_le_n n i i') + (E: n = na + nb), + exists ii, + wfo_le_n na i ii /\ + wfo_le_n nb ii i'. +Proof. + intros; ginduction na; simpl; intros; subst. + - exists i; eauto using wfo_le_refl. + - apply wfo_le_n_S' in GLE. destruct GLE as [? [? LE]]. + eapply IHna in LE; eauto. + destruct LE as [ii []]. + exists ii; eauto; split; eauto using wfo_le_n_S_rev. +Qed. + +(* ** + wfo_nat +*) + +Fixpoint wfo_nat {o : awfo} (n: nat) : wfo_set o := + match n with + | 0 => wfo_zero + | S n' => wfo_add wfo_one (wfo_nat n') + end. + +Lemma wfo_le_n_add: forall o n (i: wfo_set o), + wfo_le_n n i (wfo_add (wfo_nat n) i). +Proof. + induction n; eauto using wfo_add_lt_left, wfo_add_one, wfo_le_refl, wfo_add_proj_right. +Qed. + +Lemma wfo_nat_le_mon: forall o n m + (LE: n <= m), + @wfo_le o (wfo_nat n) (wfo_nat m). +Proof. + intros. induction LE; eauto using wfo_le_le_le, wfo_add_proj_right, wfo_le_refl. +Qed. + +Lemma wfo_nat_lt_mon: forall o n m + (LE: n < m), + @wfo_lt o (wfo_nat n) (wfo_nat m). +Proof. + intros; induction LE; eauto using wfo_lt_le_lt, wfo_lt_le, wfo_add_one. +Qed. -Arguments wfo_lt {_} _ _. -Arguments wfo_le {_} _ _. -Arguments wfo_zero {_}. -Arguments wfo_one {_}. -Arguments wfo_add {_} _ _. (* ** General Wellfounded Order in NtNnWfPoMonoid *) -Definition gwf_set : Type := list (sigT bwfo_set). +(* GWF List *) -Definition gwfel (o: bwfo) (x: o) := +Definition gwfL_set : Type := list (sigT bwfo_set). + +Definition gwfLel (o: bwfo) (x: o) := existT _ o x. Program Definition unit_wfo : bwfo := @@ -271,153 +469,153 @@ Program Definition unit_wfo : bwfo := |}. Next Obligation. econstructor; intros. contradiction. Qed. -Definition gwf_one : gwf_set := - [ gwfel unit_wfo tt ]. +Definition gwfL_one : gwfL_set := + [ gwfLel unit_wfo tt ]. -Inductive gwf_lex (b: bool) : gwf_set -> gwf_set -> Prop := -| gwf_lex_nil +Inductive gwfL_lex (b: bool) : gwfL_set -> gwfL_set -> Prop := +| gwfL_lex_nil (CHECK: is_true b) - : gwf_lex b [] [] -| gwf_lex_lt + : gwfL_lex b [] [] +| gwfL_lex_lt o x y i j (LT: bwfo_lt x y) (LEN: length i = length j) - : gwf_lex b (gwfel o x :: i) (gwfel o y :: j) -| gwf_lex_step + : gwfL_lex b (gwfLel o x :: i) (gwfLel o y :: j) +| gwfL_lex_step o x y i j (LE: bwfo_le x y) - (CMP: gwf_lex b i j) - : gwf_lex b (gwfel o x :: i) (gwfel o y :: j) -. -Hint Constructors gwf_lex. + (CMP: gwfL_lex b i j) + : gwfL_lex b (gwfLel o x :: i) (gwfLel o y :: j) +. +Hint Constructors gwfL_lex. -Variant gwf_cmp b : gwf_set -> gwf_set -> Prop := -| gwf_cmp_lt +Variant gwfL_cmp b : gwfL_set -> gwfL_set -> Prop := +| gwfL_cmp_lt o1 o2 (LEN: length o1 < length o2) - : gwf_cmp b o1 o2 -| gwf_cmp_lex + : gwfL_cmp b o1 o2 +| gwfL_cmp_lex i j - (CMP: gwf_lex b i j) - : gwf_cmp b i j + (CMP: gwfL_lex b i j) + : gwfL_cmp b i j . -Hint Constructors gwf_cmp. +Hint Constructors gwfL_cmp. -Lemma gwf_lex_length b o1 o2 - (LT: gwf_lex b o1 o2) +Lemma gwfL_lex_length b o1 o2 + (LT: gwfL_lex b o1 o2) : length o1 = length o2. Proof. intros. induction LT; simpl; nia. -Qed. +Qed. -Lemma gwf_cmp_length b o1 o2 - (CMP: gwf_cmp b o1 o2) +Lemma gwfL_cmp_length b o1 o2 + (CMP: gwfL_cmp b o1 o2) : length o1 <= length o2. Proof. destruct CMP. - nia. - - erewrite gwf_lex_length; eauto. + - erewrite gwfL_lex_length; eauto. Qed. -Lemma gwf_lex_refl: forall i, gwf_lex true i i. +Lemma gwfL_lex_refl: forall i, gwfL_lex true i i. Proof. induction i; eauto. - destruct a. eapply gwf_lex_step; eauto using bwfo_le_refl. + destruct a. eapply gwfL_lex_step; eauto using bwfo_le_refl. Qed. -Lemma gwf_le_refl: forall i, gwf_cmp true i i. +Lemma gwfL_le_refl: forall i, gwfL_cmp true i i. Proof. - intros. apply gwf_cmp_lex. eauto using gwf_lex_refl. + intros. apply gwfL_cmp_lex. eauto using gwfL_lex_refl. Qed. -Lemma gwf_lex_lt_le: forall i j, gwf_lex false i j -> gwf_lex true i j. +Lemma gwfL_lex_lt_le: forall i j, gwfL_lex false i j -> gwfL_lex true i j. Proof. intros. induction H; eauto. Qed. -Lemma gwf_lt_le: forall i j, gwf_cmp false i j -> gwf_cmp true i j. +Lemma gwfL_lt_le: forall i j, gwfL_cmp false i j -> gwfL_cmp true i j. Proof. - intros. destruct H; eauto using gwf_lex_lt_le. + intros. destruct H; eauto using gwfL_lex_lt_le. Qed. -Lemma gwf_lex_trans b1 b2 b3 i j k +Lemma gwfL_lex_trans b1 b2 b3 i j k (COND: is_true (b1 && b2) -> is_true b3) - (CMP1: gwf_lex b1 i j) - (CMP2: gwf_lex b2 j k) - : gwf_lex b3 i k. + (CMP1: gwfL_lex b1 i j) + (CMP2: gwfL_lex b2 j k) + : gwfL_lex b3 i k. Proof. ginduction CMP2; intros. - inversion CMP1; subst. destruct b1, b2, b3; eauto. - dependent destruction CMP1. - + eapply gwf_lex_lt; eauto using bwfo_le_lt_lt, bwfo_lt_le. + + eapply gwfL_lex_lt; eauto using bwfo_le_lt_lt, bwfo_lt_le. nia. - + eapply gwf_lex_lt; eauto using bwfo_le_lt_lt. - apply gwf_lex_length in CMP1. nia. + + eapply gwfL_lex_lt; eauto using bwfo_le_lt_lt. + apply gwfL_lex_length in CMP1. nia. - dependent destruction CMP1. - + eapply gwf_lex_lt; eauto using bwfo_lt_le_lt. - apply gwf_lex_length in CMP2. nia. - + eapply gwf_lex_step; eauto using bwfo_le_le_le. + + eapply gwfL_lex_lt; eauto using bwfo_lt_le_lt. + apply gwfL_lex_length in CMP2. nia. + + eapply gwfL_lex_step; eauto using bwfo_le_le_le. Qed. -Lemma gwf_cmp_trans b1 b2 b3 i j k - (CMP1: gwf_cmp b1 i j) - (CMP2: gwf_cmp b2 j k) +Lemma gwfL_cmp_trans b1 b2 b3 i j k + (CMP1: gwfL_cmp b1 i j) + (CMP2: gwfL_cmp b2 j k) (COND: is_true (b1 && b2) -> is_true b3) - : gwf_cmp b3 i k. + : gwfL_cmp b3 i k. Proof. - assert (LE1 := gwf_cmp_length CMP1). - assert (LE2 := gwf_cmp_length CMP2). - destruct CMP1, CMP2; eauto using gwf_lex_trans; apply gwf_cmp_lt; nia. + assert (LE1 := gwfL_cmp_length CMP1). + assert (LE2 := gwfL_cmp_length CMP2). + destruct CMP1, CMP2; eauto using gwfL_lex_trans; apply gwfL_cmp_lt; nia. Qed. -Lemma gwf_add_cmp_left b: forall i i' j (LE: gwf_cmp b i i'), gwf_cmp b (i ++ j) (i' ++ j). +Lemma gwfL_add_cmp_left b: forall i i' j (LE: gwfL_cmp b i i'), gwfL_cmp b (i ++ j) (i' ++ j). Proof. intros. inversion LE; subst. - - apply gwf_cmp_lt. rewrite !app_length. nia. - - apply gwf_cmp_lex. + - apply gwfL_cmp_lt. rewrite !app_length. nia. + - apply gwfL_cmp_lex. induction CMP; simpl. - + destruct b; inversion CHECK. eauto using gwf_lex_refl. - + apply gwf_lex_lt; eauto. + + destruct b; inversion CHECK. eauto using gwfL_lex_refl. + + apply gwfL_lex_lt; eauto. rewrite !app_length. nia. - + apply gwf_lex_step; eauto. + + apply gwfL_lex_step; eauto. Qed. -Lemma gwf_add_cmp_right b: forall i j j' (LE: gwf_cmp b j j'), gwf_cmp b (i ++ j) (i ++ j'). +Lemma gwfL_add_cmp_right b: forall i j j' (LE: gwfL_cmp b j j'), gwfL_cmp b (i ++ j) (i ++ j'). Proof. intros. inversion LE; subst. - - apply gwf_cmp_lt. rewrite !app_length. nia. - - apply gwf_cmp_lex. + - apply gwfL_cmp_lt. rewrite !app_length. nia. + - apply gwfL_cmp_lex. ginduction CMP; simpl; intros. - + destruct b; inversion CHECK. eauto using gwf_lex_refl. + + destruct b; inversion CHECK. eauto using gwfL_lex_refl. + induction i0; simpl; eauto. destruct a; eauto using bwfo_le_refl. + induction i0; simpl; eauto. destruct a; eauto using bwfo_le_refl. Qed. -Lemma gwf_acc_le: forall i j (WF: Acc (gwf_cmp false) i) (LE: gwf_cmp true j i), - Acc (gwf_cmp false) j. +Lemma gwfL_acc_le: forall i j (WF: Acc (gwfL_cmp false) i) (LE: gwfL_cmp true j i), + Acc (gwfL_cmp false) j. Proof. - econstructor. intros. eapply WF. eauto using gwf_cmp_trans. + econstructor. intros. eapply WF. eauto using gwfL_cmp_trans. Qed. -Lemma gwf_lt_bottom: forall i, gwf_cmp false i [] -> False. +Lemma gwfL_lt_bottom: forall i, gwfL_cmp false i [] -> False. Proof. intros. inversion H; subst. - inversion LEN. - inversion CMP. inversion CHECK. Qed. - -Lemma gwf_wf: well_founded (gwf_cmp false). + +Lemma gwfL_wf: well_founded (gwfL_cmp false). Proof. - cut (forall n i (LEon: length i <= n), Acc (gwf_cmp false) i). + cut (forall n i (LEon: length i <= n), Acc (gwfL_cmp false) i). { red; eauto. } induction n; intros. { destruct i; inversion LEon. - econstructor. intros. exfalso. eauto using gwf_lt_bottom. } + econstructor. intros. exfalso. eauto using gwfL_lt_bottom. } destruct i. - { econstructor. intros. exfalso. eauto using gwf_lt_bottom. } + { econstructor. intros. exfalso. eauto using gwfL_lt_bottom. } destruct s as [o x]. revert i LEon. simpl. assert (WFx := bwfo_wf _ x). @@ -427,218 +625,126 @@ Proof. { simpl in *. eapply IHn. nia. } dependent destruction CMP. { eapply HYPx; eauto. nia. } - - assert (WF: Acc (gwf_cmp false) i0). - { apply gwf_lex_length in CMP. eapply IHn. nia. } + + assert (WF: Acc (gwfL_cmp false) i0). + { apply gwfL_lex_length in CMP. eapply IHn. nia. } revert x0 LE. induction WF as [j _ HYPj]. econstructor. intros k LTk. - assert (LEN := gwf_lex_length CMP). + assert (LEN := gwfL_lex_length CMP). dependent destruction LTk. { simpl in *. eapply IHn. nia. } dependent destruction CMP0. { eapply HYPx; eauto using bwfo_lt_le_lt. nia. } eapply HYPj; eauto using bwfo_le_le_le. - eapply gwf_lex_trans; eauto; eauto. + eapply gwfL_lex_trans; eauto; eauto. Qed. -Program Definition gwfo : awfo := - {| wfo_set := gwf_set; - wfo_le x y := gwf_cmp true x y; - wfo_lt x y := gwf_cmp false x y; +Program Definition gwfLo : awfo := + {| wfo_set := gwfL_set; + wfo_le x y := gwfL_cmp true x y; + wfo_lt x y := gwfL_cmp false x y; wfo_zero := nil; - wfo_one := gwf_one; + wfo_one := gwfL_one; wfo_add x y := x ++ y; |}. -Next Obligation. eauto using gwf_le_refl. Qed. -Next Obligation. eauto using gwf_le_refl. Qed. -Next Obligation. rewrite app_nil_r. eauto using gwf_le_refl. Qed. -Next Obligation. rewrite app_nil_r. eauto using gwf_le_refl. Qed. -Next Obligation. rewrite app_assoc. eauto using gwf_le_refl. Qed. -Next Obligation. rewrite app_assoc. eauto using gwf_le_refl. Qed. -Next Obligation. eauto using gwf_le_refl. Qed. -Next Obligation. eauto using gwf_lt_le. Qed. -Next Obligation. eauto using gwf_cmp_trans. Qed. -Next Obligation. eauto using gwf_cmp_trans. Qed. -Next Obligation. eauto using gwf_cmp_trans. Qed. -Next Obligation. eauto using gwf_add_cmp_left. Qed. -Next Obligation. eauto using gwf_add_cmp_right. Qed. -Next Obligation. eauto using gwf_add_cmp_left. Qed. -Next Obligation. eauto using gwf_add_cmp_right. Qed. -Next Obligation. eauto using gwf_wf. Qed. +Next Obligation. eauto using gwfL_le_refl. Qed. +Next Obligation. eauto using gwfL_le_refl. Qed. +Next Obligation. rewrite app_nil_r. eauto using gwfL_le_refl. Qed. +Next Obligation. rewrite app_nil_r. eauto using gwfL_le_refl. Qed. +Next Obligation. rewrite app_assoc. eauto using gwfL_le_refl. Qed. +Next Obligation. rewrite app_assoc. eauto using gwfL_le_refl. Qed. +Next Obligation. eauto using gwfL_le_refl. Qed. +Next Obligation. eauto using gwfL_lt_le. Qed. +Next Obligation. eauto using gwfL_cmp_trans. Qed. +Next Obligation. eauto using gwfL_cmp_trans. Qed. +Next Obligation. eauto using gwfL_cmp_trans. Qed. +Next Obligation. eauto using gwfL_add_cmp_left. Qed. +Next Obligation. eauto using gwfL_add_cmp_right. Qed. +Next Obligation. eauto using gwfL_add_cmp_left. Qed. +Next Obligation. eauto using gwfL_add_cmp_right. Qed. +Next Obligation. eauto using gwfL_wf. Qed. Next Obligation. destruct i; eauto. econstructor. simpl. nia. Qed. (* ** embedding and properties *) -Definition gwf_embed {o: bwfo} (a: o) : gwfo := - [ gwfel o a ]. +Definition gwfL_embed {o: bwfo} (a: o) : gwfLo := + [ gwfLel o a ]. -Lemma gwf_embed_le_preserve (o: bwfo) (a b: o) +Lemma gwfL_embed_le_preserve (o: bwfo) (a b: o) (LT: bwfo_le a b): - wfo_le (gwf_embed a) (gwf_embed b). + wfo_le (gwfL_embed a) (gwfL_embed b). Proof. - repeat red. unfold gwf_embed. eauto. + repeat red. unfold gwfL_embed. eauto. Qed. -Lemma gwf_embed_lt_preserve (o: bwfo) (a b: o) +Lemma gwfL_embed_lt_preserve (o: bwfo) (a b: o) (LT: bwfo_lt a b): - wfo_lt (gwf_embed a) (gwf_embed b). + wfo_lt (gwfL_embed a) (gwfL_embed b). Proof. - repeat red. unfold gwf_embed. eauto. + repeat red. unfold gwfL_embed. eauto. Qed. -Lemma gwf_embed_reflect (o: bwfo) (a b: o) - (LT: wfo_lt (gwf_embed a) (gwf_embed b)): - bwfo_lt a b. +Lemma gwfL_embed_le_reflect (o: bwfo) (a b: o) + (LT: wfo_le (gwfL_embed a) (gwfL_embed b)): + bwfo_le a b. Proof. - repeat red in LT. unfold gwf_embed in *. dependent destruction LT; eauto. + repeat red in LT. unfold gwfL_embed in *. dependent destruction LT; eauto. - simpl in *. nia. - - dependent destruction CMP; eauto. - inversion CMP. inversion CHECK. + - dependent destruction CMP; eauto using bwfo_lt_le. Qed. -(* ** - Simple Properties about Orders - *) - -Lemma wfo_lt_neq: forall a i, ~ @wfo_lt a i i. -Proof. - intros. assert (WF := wfo_wf a i). red. - induction WF. eauto. -Qed. - -Lemma wfo_add_monotone: forall (a: awfo) (i i' j j': a) - (LEi: wfo_le i i') - (LEj: wfo_le j j'), - wfo_le (wfo_add i j) (wfo_add i' j'). -Proof. - eauto using wfo_le_le_le, wfo_add_le_left, wfo_add_le_right. -Qed. - -Lemma wfo_add_proj_left: forall a i j, @wfo_le a i (wfo_add i j). -Proof. - eauto using wfo_le_le_le, wfo_add_zero_r_ge, wfo_add_le_right, wfo_non_negative. -Qed. - -Lemma wfo_add_proj_right: forall a i j, @wfo_le a j (wfo_add i j). -Proof. - eauto using wfo_le_le_le, wfo_add_zero_l_ge, wfo_add_le_left, wfo_non_negative. -Qed. - -Lemma wfo_add_one: forall (a: awfo) (i: a), wfo_lt i (wfo_add wfo_one i). -Proof. - eauto using wfo_le_lt_lt, wfo_add_proj_right, wfo_add_lt_left, wfo_non_trivial. -Qed. - -(** [wfo_le_n n o o'] means that [o'] can be decreased at least [n] times - before reaching [o]. -*) -Inductive wfo_le_n {o: awfo} : nat -> o -> o -> Prop := -| wfo_le_n_Z i j (LE: wfo_le i j) - : wfo_le_n O i j -| wfo_le_n_S n i j k (GLE: wfo_le_n n i j) (LT: wfo_lt j k) - : wfo_le_n (S n) i k -. -Hint Constructors wfo_le_n. - -Lemma wfo_le_n_lt: forall o n (i i': wfo_set o) - (LE: wfo_le_n (S n) i i'), - wfo_lt i i'. -Proof. - induction n; intros; inversion LE; subst. - - inversion GLE; subst. eauto using wfo_le_lt_lt. - - apply IHn in GLE. eauto using wfo_lt_le, wfo_lt_le_lt. -Qed. - -(* TODO rename (D) *) -Lemma wfo_le_n_S': forall o n (i i': wfo_set o) - (LE: wfo_le_n (S n) i i'), - exists j : wfo_set o, - wfo_lt i j /\ - wfo_le_n n j i'. +Lemma gwfL_embed_lt_reflect (o: bwfo) (a b: o) + (LT: wfo_lt (gwfL_embed a) (gwfL_embed b)): + bwfo_lt a b. Proof. - induction n; intros; inversion LE; subst. - - inversion GLE. subst. eauto using wfo_le_lt_lt, wfo_le_refl. - - edestruct IHn; eauto. - destruct H. eauto. + repeat red in LT. unfold gwfL_embed in *. dependent destruction LT; eauto. + - simpl in *. nia. + - dependent destruction CMP; eauto. + inversion CMP. inversion CHECK. Qed. -Lemma wfo_le_n_S'': forall o n (i i': wfo_set o) - (LE: wfo_le_n (S n) i i'), - wfo_le_n n i i'. -Proof. - intros; inversion LE; inversion GLE; subst; eauto using wfo_lt_le, wfo_le_le_le, wfo_lt_le_lt. -Qed. +(* GWF *) -Lemma wfo_le_n_wfo_le: forall o n (i i' i'': wfo_set o) - (GLE: wfo_le_n n i i') - (LE: wfo_le i' i''), - wfo_le_n n i i''. -Proof. - intros; dependent destruction GLE; [econstructor 1|econstructor 2]; eauto using wfo_le_le_le, wfo_lt_le_lt. -Qed. +Definition gwfo := awfo_lexprod gwfLo gwfLo. -Lemma wfo_le_n_anti: forall o m n (i i': wfo_set o) - (GLE: wfo_le_n m i i') - (LE: n <= m), - wfo_le_n n i i'. -Proof. - intros; ginduction LE; eauto. - intros; apply IHLE; auto using wfo_le_n_S''. -Qed. +Definition gwf_embed {o: bwfo} (a: o) : gwfo := + (wfo_zero, gwfL_embed a). -(* TODO rename *) -Lemma wfo_le_n_S_rev: forall o (i j: wfo_set o) n k - (LT: wfo_lt i j) - (GLE: wfo_le_n n j k), - wfo_le_n (S n) i k. +Lemma gwf_embed_le_preserve (o: bwfo) (a b: o) + (LT: bwfo_le a b): + wfo_le (gwf_embed a) (gwf_embed b). Proof. - intros; ginduction GLE; intros; eauto. - econstructor; eauto using wfo_lt_le_lt, wfo_le_refl. + econstructor 2. simpl. split; eauto. + eapply gwfL_embed_le_preserve; eauto. Qed. -Lemma wfo_le_n_plus: forall o n na nb (i i': wfo_set o) - (GLE: wfo_le_n n i i') - (E: n = na + nb), - exists ii, - wfo_le_n na i ii /\ - wfo_le_n nb ii i'. +Lemma gwf_embed_lt_preserve (o: bwfo) (a b: o) + (LT: bwfo_lt a b): + wfo_lt (gwf_embed a) (gwf_embed b). Proof. - intros; ginduction na; simpl; intros; subst. - - exists i; eauto using wfo_le_refl. - - apply wfo_le_n_S' in GLE. destruct GLE as [? [? LE]]. - eapply IHna in LE; eauto. - destruct LE as [ii []]. - exists ii; eauto; split; eauto using wfo_le_n_S_rev. + econstructor 2. simpl. split; eauto. + eapply gwfL_embed_lt_preserve; eauto. Qed. -(* ** - wfo_nat -*) - -Fixpoint wfo_nat {o : awfo} (n: nat) : wfo_set o := - match n with - | 0 => wfo_zero - | S n' => wfo_add wfo_one (wfo_nat n') - end. - -Lemma wfo_le_n_add: forall o n (i: wfo_set o), - wfo_le_n n i (wfo_add (wfo_nat n) i). +Lemma gwf_embed_le_reflect (o: bwfo) (a b: o) + (LT: wfo_le (gwf_embed a) (gwf_embed b)): + bwfo_le a b. Proof. - induction n; eauto using wfo_add_lt_left, wfo_add_one, wfo_le_refl, wfo_add_proj_right. + eapply gwfL_embed_le_reflect. + inversion LT. + - simpl in *. exfalso. eauto using gwfL_lt_bottom. + - destruct H. eauto. Qed. -Lemma wfo_nat_le_mon: forall o n m - (LE: n <= m), - @wfo_le o (wfo_nat n) (wfo_nat m). +Lemma gwf_embed_lt_reflect (o: bwfo) (a b: o) + (LT: wfo_lt (gwf_embed a) (gwf_embed b)): + bwfo_lt a b. Proof. - intros. induction LE; eauto using wfo_le_le_le, wfo_add_proj_right, wfo_le_refl. + eapply gwfL_embed_lt_reflect. + inversion LT. + - simpl in *. exfalso. eauto using gwfL_lt_bottom. + - destruct H. eauto. Qed. -Lemma wfo_nat_lt_mon: forall o n m - (LE: n < m), - @wfo_lt o (wfo_nat n) (wfo_nat m). -Proof. - intros; induction LE; eauto using wfo_lt_le_lt, wfo_lt_le, wfo_add_one. -Qed. diff --git a/theories/Eq/Eq.v b/theories/Eq/Eq.v index 502c2bfa..a619cd37 100644 --- a/theories/Eq/Eq.v +++ b/theories/Eq/Eq.v @@ -1031,7 +1031,9 @@ Proof. destruct REL. eauto using eqiti_lower_order. Qed. Lemma euttOrd_small n (so: euttOrdWf) : wfo_lt (gwf_embed so) (wfo_nat (S (S n))). Proof. - econstructor. simpl. nia. + econstructor 2. split. + - simpl. induction n; eauto. + - econstructor. simpl. nia. Qed. Lemma eq_itree_zero {E} b1 b2 R1 R2 RR t1 t2