From 73df1945b31c0beee88cf4476df4ccd09d31403b Mon Sep 17 00:00:00 2001 From: Rutger Broekhoff Date: Wed, 26 Jun 2024 20:50:18 +0200 Subject: Import Coq project --- semprop.v | 426 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 426 insertions(+) create mode 100644 semprop.v (limited to 'semprop.v') diff --git a/semprop.v b/semprop.v new file mode 100644 index 0000000..3af718d --- /dev/null +++ b/semprop.v @@ -0,0 +1,426 @@ +Require Import Coq.Strings.String. +From stdpp Require Import gmap option tactics. +From mininix Require Import binop expr maptools matching relations sem. + +Lemma ctx_item_inj E uf_ext uf_int : + is_ctx_item uf_ext uf_int E → + Inj (=) (=) E. +Proof. + intros Hctx. + destruct Hctx; intros e1' e2' Hinj; try congruence. + injection Hinj as Hinj. + by apply map_insert_rev_1_L in Hinj. +Qed. + +Global Instance id_inj {A} : Inj (=) (=) (@id A). +Proof. by unfold Inj. Qed. + +Lemma ctx_inj E uf_ext uf_int : + is_ctx uf_ext uf_int E → + Inj (=) (=) E. +Proof. + intros Hctx. + induction Hctx. + - apply id_inj. + - apply ctx_item_inj in H. + by apply compose_inj with (=). +Qed. + +Lemma base_step_deterministic : deterministic base_step. +Proof. + unfold deterministic. + intros e0 e1 e2 H1 H2. + inv H1; inv H2; try done. + - destruct ys, ys0. by simplify_eq/=. + - destruct ys. by simplify_eq/=. + - destruct ys. by simplify_eq/=. + - apply map_insert_inv in H0. by destruct H0. + - destruct ys. by simplify_eq/=. + - destruct ys. by simplify_eq/=. + - destruct ys, ys0. by simplify_eq/=. + - exfalso. apply H3. by exists bs. + - exfalso. apply H. by exists bs. + - f_equal. by eapply matches_deterministic. + - apply map_insert_inv in H0 as [H01 H02]. + by simplify_eq /=. + - f_equal. by eapply binop_deterministic. + - rewrite H4 in H. by apply is_Some_None in H. + - exfalso. apply H4. by exists bs. + - rewrite H in H4. by apply is_Some_None in H4. + - exfalso. apply H. by exists bs. +Qed. + +Reserved Notation "e '-/' uf '/->' e'" (right associativity, at level 55). + +Inductive fstep : bool → expr → expr → Prop := + | F_Ctx e1 e2 E uf_ext uf_int : + is_ctx uf_ext uf_int E → + e1 -->base e2 → + E e1 -/uf_ext/-> E e2 +where "e -/ uf /-> e'" := (fstep uf e e'). + +Hint Constructors fstep : core. + +Lemma ufstep e e' : e -/false/-> e' ↔ e --> e'. +Proof. split; intros; inv H; by econstructor. Qed. + +Lemma fstep_strongly_confluent_aux x uf y1 y2 : + x -/uf/-> y1 → + x -/uf/-> y2 → + y1 = y2 ∨ ∃ z, y1 -/uf/-> z ∧ y2 -/uf/-> z. +Proof. + intros Hstep1 Hstep2. + inv Hstep1 as [b11 b12 E1 uf_int uf_int1 Hctx1 Hbase1]. + inv Hstep2 as [b21 b22 E2 uf_int uf_int2 Hctx2 Hbase2]. + revert b11 b12 b21 b22 E2 Hbase1 Hbase2 Hctx2 H0. + induction Hctx1 as [|E1 E0]; + intros b11 b12 b21 b22 E2 Hbase1 Hbase2 Hctx2 H2; inv Hctx2. + - (* L: id, R: id *) left. by eapply base_step_deterministic. + - (* L: id, R: ∘ *) simplify_eq/=. + inv H. + + inv Hbase1. + * inv H0. + -- inv Hbase2. + -- inv H. + * inv H0. + -- inv Hbase2. + -- inv H1. inv H. + + inv Hbase1. + * inv H0. + -- inv Hbase2. + -- inv H. + * inv H0. + -- inv Hbase2. + -- inv H. + + inv Hbase1. + * inv H0. + -- inv Hbase2. + -- inv H. + * inv H0. + -- inv Hbase2. + -- inv H1. + + inv Hbase1. + * inv H0. + -- inv Hbase2. + -- inv H. + * inv H0. + -- inv Hbase2. + -- inv H1. + * inv H0. + -- inv Hbase2. + -- inv H1. inv H. + + inv Hbase1. + inv H0. + * inv Hbase2. + * inv H. + + inv Hbase1. + * inv H0. + -- inv Hbase2. + -- inv H. + * inv H0. + -- inv Hbase2. + -- inv H. + + inv Hbase1. + inv H0. + * inv Hbase2. + * inv H. + + inv Hbase1. + inv H0. + * inv Hbase2. + * inv H. + + inv Hbase1. + inv H0. + * inv Hbase2. + * inv H. + + inv Hbase1. + * inv H0. + -- inv Hbase2. + -- inv H1. + * inv H0. + -- inv Hbase2. + -- inv H1. + * inv H0. + -- inv Hbase2. + -- inv H1. + + inv Hbase1. + inv H0. + * inv Hbase2. + * inv H. + simplify_option_eq. + destruct sv; try discriminate. + exfalso. clear uf. simplify_option_eq. + apply fmap_insert_lookup in H1. simplify_option_eq. + revert bs0 x H H1 Heqo. + induction H2; intros bs0 x H' H1 Heqo. + -- inv Hbase2. + -- simplify_option_eq. + inv H. destruct H'; try discriminate. + inv H1. apply fmap_insert_lookup in H0. simplify_option_eq. + by eapply IHis_ctx. + + inv Hbase1. + - (* L: ∘, R: id *) + simplify_eq/=. + inv H. + + inv Hbase2. + * inv Hctx1. + -- inv Hbase1. + -- inv H. + * inv Hctx1. + -- inv Hbase1. + -- inv H0. inv H. + + inv Hbase2. + * inv Hctx1. + -- inv Hbase1. + -- inv H. + * inv Hctx1. + -- inv Hbase1. + -- inv H. + + inv Hbase2. + * inv Hctx1. + -- inv Hbase1. + -- inv H. + * inv Hctx1. + -- inv Hbase1. + -- inv H0. + + inv Hbase2. + * inv Hctx1. + -- inv Hbase1. + -- inv H. + * inv Hctx1. + -- inv Hbase1. + -- inv H0. + * inv Hctx1. + -- inv Hbase1. + -- inv H0. inv H. + + inv Hbase2. + inv Hctx1. + * inv Hbase1. + * inv H. + + inv Hbase2. + * inv Hctx1. + -- inv Hbase1. + -- inv H. + * inv Hctx1. + -- inv Hbase1. + -- inv H. + + inv Hbase2. + inv Hctx1. + * inv Hbase1. + * inv H. + + inv Hbase2. + inv Hctx1. + * inv Hbase1. + * inv H. + + inv Hbase2. + inv Hctx1. + * inv Hbase1. + * inv H. + + inv Hbase2. + * inv Hctx1. + -- inv Hbase1. + -- inv H0. + * inv Hctx1. + -- inv Hbase1. + -- inv H0. + * inv Hctx1. + -- inv Hbase1. + -- inv H0. + + inv Hbase2. + inv Hctx1. + * inv Hbase1. + * clear IHHctx1. + inv H. + simplify_option_eq. + destruct sv; try discriminate. + exfalso. simplify_option_eq. + apply fmap_insert_lookup in H0. simplify_option_eq. + revert bs0 x H H0 Heqo. + induction H1; intros bs0 x H' H0 Heqo. + -- inv Hbase1. + -- simplify_option_eq. + inv H. destruct H'; try discriminate. + inv H0. apply fmap_insert_lookup in H2. simplify_option_eq. + eapply IHis_ctx. + ++ apply H2. + ++ apply Heqo0. + + inv Hbase2. + - (* L: ∘, R: ∘ *) + simplify_option_eq. + inv H; inv H0. + + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2) + as [IH | [z [IHz1 IHz2]]]. + * left. congruence. + * right. exists (X_Select z xs). + split; [inv IHz1 | inv IHz2]; + eapply F_Ctx with (E := (λ e, X_Select e xs) ∘ E); try done; + by eapply IsCtx_Compose. + + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2) + as [IH | [z [IHz1 IHz2]]]. + * left. congruence. + * right. exists (X_SelectOr z xs e2). + split; [inv IHz1 | inv IHz2]; + eapply F_Ctx with (E := (λ e1, X_SelectOr e1 xs e2) ∘ E); try done; + by eapply IsCtx_Compose. + + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2) + as [IH | [z [IHz1 IHz2]]]. + * left. congruence. + * right. exists (X_Incl z e2). + split; [inv IHz1 | inv IHz2]; + eapply F_Ctx with (E := (λ e1, X_Incl e1 e2) ∘ E); try done; + by eapply IsCtx_Compose. + + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2) + as [IH | [z [IHz1 IHz2]]]. + * left. congruence. + * right. exists (X_Apply z e2). + split; [inv IHz1 | inv IHz2]; + eapply F_Ctx with (E := (λ e1, X_Apply e1 e2) ∘ E); try done; + by eapply IsCtx_Compose. + + inv Hctx1; simplify_option_eq. + * inv Hbase1. + * inv H. + + inv H1; simplify_option_eq. + * inv Hbase2. + * inv H. + + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H0) + as [IH | [z [IHz1 IHz2]]]. + * left. congruence. + * right. exists (X_Apply (V_AttrsetFn m e1) z). + split; [inv IHz1 | inv IHz2]; + eapply F_Ctx with (E := (λ e2, X_Apply (V_AttrsetFn m e1) e2) ∘ E); + try done; + by eapply IsCtx_Compose. + + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2) + as [IH | [z [IHz1 IHz2]]]. + * left. congruence. + * right. exists (X_Cond z e2 e3). + split; [inv IHz1 | inv IHz2]; + eapply F_Ctx with (E := (λ e1, X_Cond e1 e2 e3) ∘ E); try done; + by eapply IsCtx_Compose. + + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2) + as [IH | [z [IHz1 IHz2]]]. + * left. congruence. + * right. exists (X_Assert z e2). + split; [inv IHz1 | inv IHz2]; + eapply F_Ctx with (E := (λ e1, X_Assert e1 e2) ∘ E); try done; + by eapply IsCtx_Compose. + + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H) + as [IH | [z [IHz1 IHz2]]]. + * left. congruence. + * right. exists (X_Op op z e2). + split; [inv IHz1 | inv IHz2]; + eapply F_Ctx with (E := (λ e1, X_Op op e1 e2) ∘ E); try done; + by eapply IsCtx_Compose. + + inv Hctx1; simplify_option_eq. + * inv Hbase1. + * inv H0. + + inv H1; simplify_option_eq. + * inv Hbase2. + * inv H0. + + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H0) + as [IH | [z [IHz1 IHz2]]]. + * left. congruence. + * right. exists (X_Op op v1 z). + split; [inv IHz1 | inv IHz2]; + eapply F_Ctx with (E := (λ e2, X_Op op v1 e2) ∘ E); try done; + by eapply IsCtx_Compose. + + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2) + as [IH | [z [IHz1 IHz2]]]. + * left. congruence. + * right. exists (X_HasAttr z x). + split; [inv IHz1 | inv IHz2]; + eapply F_Ctx with (E := (λ e, X_HasAttr e x) ∘ E); try done; + by eapply IsCtx_Compose. + + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2) + as [IH | [z [IHz1 IHz2]]]. + * left. congruence. + * right. exists (X_Force z). + split. + -- inv IHz1. + (* apply is_ctx_uf_false_impl_true in H0 as []. *) + eapply F_Ctx with (E := X_Force ∘ E); try done; + by eapply IsCtx_Compose. + -- inv IHz2. + eapply F_Ctx with (E := X_Force ∘ E); try done; + by eapply IsCtx_Compose. + + destruct (decide (x0 = x)). + * simplify_option_eq. + apply map_insert_rev_L in H2 as [H21 H22]. + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H21) + as [IH | [z [IHz1 IHz2]]]. + -- left. rewrite IH. do 2 f_equal. + by apply map_insert_L. + -- right. exists (V_Attrset (<[x := z]>bs)). + split. + ++ inv IHz1. + eapply F_Ctx + with (E := (λ e, X_V $ V_Attrset (<[x := e]>bs)) ∘ E); try done. + by eapply IsCtx_Compose. + ++ inv IHz2. + rewrite (map_insert_L _ _ _ _ _ (eq_refl (E e1)) H22). + eapply F_Ctx + with (E := (λ e, X_V $ V_Attrset (<[x := e]>bs)) ∘ E); try done. + by eapply IsCtx_Compose. + * simplify_option_eq. + right. exists (V_Attrset (<[x := E0 b12]>(<[x0 := E4 b22]>bs))). + split. + -- apply map_insert_ne_inv in H2 as H3; try done. + destruct H3. + replace bs with (<[x0 := E4 b21]>bs) at 1; try by rewrite insert_id. + setoid_rewrite insert_commute; try by congruence. + eapply F_Ctx + with (E := (λ e, X_V $ V_Attrset + (<[x0 := e]>(<[x := E0 b12]> bs))) ∘ E4). + ++ by eapply IsCtx_Compose. + ++ done. + -- apply map_insert_ne_inv in H2 as H3; try done. + destruct H3 as [H31 [H32 H33]]. + replace bs0 with (<[x := E0 b11]>bs0) at 1; + try by rewrite insert_id. + rewrite insert_commute; try by congruence. + replace (<[x:=E0 b11]> (<[x0:=E4 b22]> bs0)) + with (<[x:=E0 b11]> (<[x0:=E4 b22]> bs)). + 2: { + rewrite <-insert_delete_insert. + setoid_rewrite <-insert_delete_insert at 2. + rewrite delete_insert_ne by congruence. + rewrite delete_commute. rewrite <-H33. + rewrite insert_delete_insert. + rewrite <-delete_insert_ne by congruence. + by rewrite insert_delete_insert. + } + eapply F_Ctx with (E := (λ e, X_V $ V_Attrset + (<[x := e]>(<[x0 := E4 b22]>bs))) ∘ E0). + ++ by eapply IsCtx_Compose. + ++ done. +Qed. + +Lemma step_strongly_confluent_aux x y1 y2 : + x --> y1 → + x --> y2 → + y1 = y2 ∨ ∃ z, y1 --> z ∧ y2 --> z. +Proof. + intros Hstep1 Hstep2. + apply ufstep in Hstep1, Hstep2. + destruct (fstep_strongly_confluent_aux _ _ _ _ Hstep1 Hstep2) as [|[?[]]]. + - by left. + - right. exists x0. split; by apply ufstep. +Qed. + +Theorem step_strongly_confluent : strongly_confluent step. +Proof. + intros x y1 y2 Hy1 Hy2. + destruct (step_strongly_confluent_aux x y1 y2 Hy1 Hy2) as [|[z [Hz1 Hz2]]]. + - exists y1. by subst. + - exists z. split. + + by apply rtc_once. + + by apply rc_once. +Qed. + +Lemma step_semi_confluent : semi_confluent step. +Proof. apply strong__semi_confluence. apply step_strongly_confluent. Qed. + +Lemma step_cr : cr step. +Proof. apply semi_confluence__cr. apply step_semi_confluent. Qed. + +Theorem step_confluent : confluent step. +Proof. apply confluent_alt. apply step_cr. Qed. -- cgit v1.2.3