From efcb60aae31021a719b8b1ade9cae32962a3284e Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Sat, 6 Jul 2024 20:44:21 +0200 Subject: [PATCH 1/3] this wont work --- minuska/theories/BuiltinValue.v | 65 ++++++++++++++++++++++++++ minuska/theories/basic_properties.v | 13 ++++++ minuska/theories/interpreter_results.v | 1 - 3 files changed, 78 insertions(+), 1 deletion(-) diff --git a/minuska/theories/BuiltinValue.v b/minuska/theories/BuiltinValue.v index 4be25e82..79694997 100644 --- a/minuska/theories/BuiltinValue.v +++ b/minuska/theories/BuiltinValue.v @@ -13,6 +13,71 @@ Section sec. {_sc : Countable symbol} . + (* This is an attempt at an alternative definition that avoids lowlang. + I could not figure out how to implement decision procedure for equality, + so it is left for future work. + + (* TODO make parametric in a user type *) + Inductive BuiltinValue0 := + | bv_error + | bv_bool (b : bool) + (* | bv_nat (n : nat) *) + | bv_Z (z : Z) + | bv_sym (s : symbol) + | bv_str (s : string) + | bv_list (m : list (@TermOver' symbol BuiltinValue0)) + | bv_pmap (m : Pmap (@TermOver' symbol BuiltinValue0)) + . + + Fixpoint BVsize (r : BuiltinValue0) : nat := + match r with + | bv_error => 1 + | bv_bool _ => 1 + | bv_Z _ => 1 + | bv_sym _ => 1 + | bv_str _ => 1 + | bv_list l => + let TermBVsize := (fix TermBVsize (t : @TermOver' symbol BuiltinValue0) : nat := + match t with + | t_over m => S (BVsize m) + | t_term _ l => S ( + (fix helper (l' : list (@TermOver' symbol BuiltinValue0)) : nat := + match l' with + | [] => 1 + | x::xs => S (TermBVsize x + helper xs) + end + )l) + end) in + S (sum_list_with TermBVsize l) + | bv_pmap PEmpty => 1 + | bv_pmap (PNodes m) => + let TermBVsize := (fix TermBVsize (t : @TermOver' symbol BuiltinValue0) : nat := + match t with + | t_over m => S (BVsize m) + | t_term _ l => S ( + (fix helper (l' : list (@TermOver' symbol BuiltinValue0)) : nat := + match l' with + | [] => 1 + | x::xs => S (TermBVsize x + helper xs) + end + )l) + end) in + S ((fix mypmsz (m' : Pmap_ne (@TermOver' symbol BuiltinValue0)) := + match m' with + | PNode001 m'' => S (mypmsz m'') + | PNode010 m'' => S (TermBVsize m'') + | PNode011 m1 m2 => S (TermBVsize m1 + mypmsz m2) + | PNode100 m'' => mypmsz m'' + | PNode101 m1 m2 => S (mypmsz m1 + mypmsz m2) + | PNode110 m1 m2 => S (mypmsz m1 + TermBVsize m2) + | PNode111 m1 m2 m3 => S (mypmsz m1 + TermBVsize m2 + mypmsz m3) + end + ) m) + end + . + + *) + (* TODO make parametric in a user type *) Inductive BuiltinValue0 := | bv_error diff --git a/minuska/theories/basic_properties.v b/minuska/theories/basic_properties.v index 40995b72..7947b00f 100644 --- a/minuska/theories/basic_properties.v +++ b/minuska/theories/basic_properties.v @@ -434,3 +434,16 @@ Lemma vars_of_t_term_e vars_of (t_term s l) = union_list ( vars_of <$> l) . Proof. reflexivity. Qed. + + +Fixpoint TermOver_size_with + {T : Type} + {A : Type} + (fsz : A -> nat) + (t : @TermOver' T A) + : nat +:= +match t with +| t_over a => fsz a +| t_term _ l => S (sum_list_with (S ∘ TermOver_size_with fsz) l) +end. diff --git a/minuska/theories/interpreter_results.v b/minuska/theories/interpreter_results.v index c7893c41..e7b865a9 100644 --- a/minuska/theories/interpreter_results.v +++ b/minuska/theories/interpreter_results.v @@ -6,7 +6,6 @@ From Minuska Require Import syntax_properties semantics_properties spec_interpreter - basic_matching . From ae59120a8dd9083f809421c97cb1e520443e00d2 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Sat, 6 Jul 2024 21:09:33 +0200 Subject: [PATCH 2/3] remove some stuff --- minuska/_CoqProject | 1 - minuska/theories/basic_matching.v | 1649 ------------ minuska/theories/minusl_compile_properties.v | 2421 +----------------- 3 files changed, 135 insertions(+), 3936 deletions(-) diff --git a/minuska/_CoqProject b/minuska/_CoqProject index 17bdfb65..97854213 100644 --- a/minuska/_CoqProject +++ b/minuska/_CoqProject @@ -16,7 +16,6 @@ theories/minuska.v theories/string_variables.v theories/BuiltinValue.v theories/builtins.v -theories/basic_matching.v theories/try_match.v theories/naive_interpreter.v theories/interpreter_results.v diff --git a/minuska/theories/basic_matching.v b/minuska/theories/basic_matching.v index de66df47..b09adefe 100644 --- a/minuska/theories/basic_matching.v +++ b/minuska/theories/basic_matching.v @@ -1,1653 +1,4 @@ From Minuska Require Import prelude - spec - lowlang - syntax_properties - semantics_properties - properties . - -Require Import Logic.PropExtensionality. -Require Import Setoid. -Require Import Coq.Classes.Morphisms. -Require Import Coq.Classes.Morphisms_Prop. - - -#[local] -Unset Transparent Obligations. - -Definition valuation_restrict - {Σ : StaticModel} - {var : Type} - {_varED : EqDecision var} - {_varCnt : Countable var} - (ρ : (gmap var GroundTerm)) - (r : gset var) - : gmap var GroundTerm -:= - filter - (λ x : var * GroundTerm, x.1 ∈ r) - ρ -. - -Lemma valuation_restrict_eq_subseteq - {Σ : StaticModel} - {var : Type} - {_varED : EqDecision var} - {_varCnt : Countable var} - (ρ1 ρ2 : (gmap var GroundTerm)) - (r r' : gset var) -: - r ⊆ r' -> - valuation_restrict ρ1 r' = valuation_restrict ρ2 r' -> - valuation_restrict ρ1 r = valuation_restrict ρ2 r -. -Proof. - intros H1 H2. - unfold valuation_restrict in *. - rewrite map_eq_iff. - rewrite map_eq_iff in H2. - intros x. - specialize (H2 x). - do 2 (rewrite map_lookup_filter in H2). - do 2 (rewrite map_lookup_filter). - simpl in *. - rewrite elem_of_subseteq in H1. - specialize (H1 x). - simpl in *. - ltac1:(case_guard as Hcg1; case_guard as Hcg2); simpl in *; try ltac1:(auto with nocore). - { - destruct (ρ1 !! x) eqn:Hρ1x, (ρ2 !! x) eqn:Hρ2x; simpl in *; - reflexivity. - } - { - ltac1:(exfalso). - ltac1:(auto with nocore). - } -Qed. - -Lemma valuation_restrict_eq_impl_lookup - {Σ : StaticModel} - {var : Type} - {_varED : EqDecision var} - {_varCnt : Countable var} - (ρ1 ρ2 : (gmap var GroundTerm)) - (r : gset var) - (x : var) - : - x ∈ r -> - valuation_restrict ρ1 r = valuation_restrict ρ2 r -> - ρ1 !! x = ρ2 !! x -. -Proof. - intros H1 H2. - unfold valuation_restrict in H2. - rewrite map_eq_iff in H2. - specialize (H2 x). - do 2 (rewrite map_lookup_filter in H2). - destruct (ρ1 !! x) eqn:Hρ1x, (ρ2 !! x) eqn:Hρ2x; simpl in *; - ltac1:(simplify_eq/=; repeat case_guard; simplify_eq/=); - (auto with nocore); try reflexivity; ltac1:(try solve[exfalso; auto]). -Qed. - -Class Matches - {Σ : StaticModel} - (A B var : Type) - {_varED : EqDecision var} - {_varCnt : Countable var} - {_VA : VarsOf B var} - {_SAB : Satisfies (gmap var GroundTerm) A B var} := -{ - matchesb: - (gmap var GroundTerm) -> A -> B -> bool ; - - satisfies_matchesb : - ∀ (v : (gmap var GroundTerm)) (a : A) (b : B), - (satisfies v a b) -> (matchesb v a b = true) ; - - matchesb_satisfies : - ∀ (v : (gmap var GroundTerm)) (a : A) (b : B), - (matchesb v a b = true) -> (satisfies v a b) ; - - matchesb_vars_of : - ∀ (v : (gmap var GroundTerm)) (a : A) (b : B), - matchesb v a b = true -> - vars_of b ⊆ vars_of v ; - - matchesb_insensitive : - ∀ (v1 v2 : (gmap var GroundTerm)) (a : A) (b : B), - valuation_restrict v1 (vars_of b) = valuation_restrict v2 (vars_of b) -> - matchesb v1 a b = matchesb v2 a b ; -}. -(* Set Typeclasses Debug. *) -Arguments satisfies : simpl never. -Arguments matchesb : simpl never. - -Lemma matchesb_ext - {Σ : StaticModel} - (A B var : Type) - {_varED : EqDecision var} - {_varCnt : Countable var} - {_VA : VarsOf B var} - {_SAB : Satisfies (gmap var GroundTerm) A B var} - {_SPAB : SatisfiesProperties (gmap var GroundTerm) A B var} - {_MAB : Matches A B var} - : - forall (v1 v2 : (gmap var GroundTerm)), - v1 ⊆ v2 -> - forall (a : A) (b : B), - matchesb v1 a b = true -> - matchesb v2 a b = true -. -Proof. - intros. - apply matchesb_satisfies in H0. - apply satisfies_matchesb. - eapply satisfies_ext. - { exact H. } - { assumption. } -Qed. - -Section with_signature. - Context - {Σ : StaticModel} - . - - Fixpoint ApppliedOperator'_matches_PreTerm' - {Operand1 Operand2 var : Type} - {_varED : EqDecision var} - {_varCnt : Countable var} - {_S1 : Satisfies (gmap var GroundTerm) (symbol) Operand2 var} - {_S2 : Satisfies (gmap var GroundTerm) (Operand1) Operand2 var} - {_S3 : Satisfies (gmap var GroundTerm) (Operand1) (PreTerm' symbol Operand2) var} - {_S4 : Satisfies (gmap var GroundTerm) (PreTerm' symbol Operand1) Operand2 var} - {_V1 : VarsOf Operand1 var} - {_V2 : VarsOf Operand2 var} - {_M1 : Matches (symbol) Operand2 var} - {_M2 : Matches (Operand1) Operand2 var} - {_M3 : Matches (Operand1) (PreTerm' symbol Operand2) var} - {_M4 : Matches (PreTerm' symbol Operand1) Operand2 var} - (ρ : (gmap var GroundTerm)) - (x : (PreTerm' symbol Operand1)) - (y : PreTerm' symbol Operand2) - : bool := - match x, y with - | pt_operator a1, pt_operator a2 => - bool_decide (a1 = a2) - | pt_operator _, pt_app_operand _ _ => false - | pt_operator _, pt_app_ao _ _ => false - | pt_app_operand _ _ , pt_operator _ => false - | pt_app_operand app1 o1, pt_app_operand app2 o2 => - ApppliedOperator'_matches_PreTerm' - ρ (app1) - app2 - && matchesb ρ (o1) o2 - | pt_app_operand app1 o1, pt_app_ao app2 o2 => - ApppliedOperator'_matches_PreTerm' ρ app1 app2 - && matchesb ρ o1 o2 - | pt_app_ao app1 o1, pt_operator _ => false - | pt_app_ao app1 o1, pt_app_operand app2 o2 => - ApppliedOperator'_matches_PreTerm' - ρ app1 - app2 - && matchesb ρ o1 o2 - | pt_app_ao app1 o1, pt_app_ao app2 o2 => - ApppliedOperator'_matches_PreTerm' - ρ app1 - app2 - && - ApppliedOperator'_matches_PreTerm' - ρ o1 - o2 - end. - - Lemma vars_of_filter - {var B : Type} - {_EV : EqDecision var} - {_CV : Countable var} - {_VB : VarsOf B var} - (b' : B) - (v1 : gmap var GroundTerm) - : - vars_of (filter (λ x : var * GroundTerm, x.1 ∈ vars_of b') v1) - ⊆ vars_of b' - . - Proof. - rewrite elem_of_subseteq. - intros v Hv. - unfold vars_of in Hv; simpl in Hv. - rewrite elem_of_dom in Hv. - destruct Hv as [w Hw]. - rewrite map_lookup_filter in Hw. - rewrite bind_Some in Hw. - destruct Hw as [g [H1g H2g]]. - ltac1:(repeat case_guard; simpl in *; simplify_eq/=). - assumption. - Qed. - - - - Lemma vars_of_filter_2 - {var B : Type} - {_EV : EqDecision var} - {_CV : Countable var} - {_VB : VarsOf B var} - (b' : B) - (v1 : gmap var GroundTerm) - : - vars_of (filter (λ x : var * GroundTerm, x.1 ∈ vars_of b') v1) - ⊆ vars_of v1 - . - Proof. - rewrite elem_of_subseteq. - intros v Hv. - unfold vars_of in Hv at 1; simpl in Hv. - rewrite elem_of_dom in Hv. - destruct Hv as [w Hw]. - rewrite map_lookup_filter in Hw. - rewrite bind_Some in Hw. - destruct Hw as [g [H1g H2g]]. - ltac1:(repeat case_guard; simpl in *; simplify_eq/=). - unfold vars_of; simpl. - rewrite elem_of_dom. - exists w. assumption. - Qed. - - - #[export] - Program Instance reflect__satisfies__ApppliedOperator'_matches_PreTerm' - {Operand1 Operand2 var : Type} - {_varED : EqDecision var} - {_varCnt : Countable var} - {_V1v : VarsOf Operand1 var} - {_V2v : VarsOf Operand2 var} - {_S1 : Satisfies (gmap var GroundTerm) (symbol) Operand2 var} - {_S2 : Satisfies (gmap var GroundTerm) (Operand1) Operand2 var} - {_S3 : Satisfies (gmap var GroundTerm) (Operand1) (PreTerm' symbol Operand2) var} - {_S4 : Satisfies (gmap var GroundTerm) (PreTerm' symbol Operand1) Operand2 var} - {_M1 : Matches (symbol) Operand2 var} - {_M2 : Matches (Operand1) Operand2 var} - {_M3 : Matches (Operand1) (PreTerm' symbol Operand2) var} - {_M4 : Matches (PreTerm' symbol Operand1) Operand2 var} - : - Matches - ((PreTerm' symbol Operand1)) - (PreTerm' symbol Operand2) - var - := {| - matchesb := - ApppliedOperator'_matches_PreTerm' ; - matchesb_satisfies := _; - satisfies_matchesb := _; - |}. - Next Obligation. - simpl. - ltac1:(rename v into ρ). - ltac1:(rename a into x). - ltac1:(rename b into y). - revert y X. - induction x; intros y X; destruct y. - { - simpl. - unfold bool_decide. - ltac1:(case_match). - { - subst. - constructor. - } - { - inversion X; subst. - ltac1:(congruence). - } - } - { - inversion X; subst; clear X. - } - { - inversion X; subst; clear X. - } - { - inversion X; subst; clear X. - } - { - inversion X; subst; clear X. - simpl. - unfold is_true. - rewrite andb_true_iff. - split. - { - apply IHx. apply X0. - } - { - apply satisfies_matchesb in X1. - apply X1. - } - } - { - inversion X; subst; clear X. - simpl. - unfold is_true. - rewrite andb_true_iff. - split. - { - apply IHx. apply X0. - } - { - apply satisfies_matchesb in X1. - apply X1. - } - } - { - inversion X; subst; clear X. - } - { - inversion X; subst; clear X. - simpl. - unfold is_true. - rewrite andb_true_iff. - split. - { - apply IHx1. apply X0. - } - { - apply satisfies_matchesb in X1. - apply X1. - } - } - { - inversion X; subst; clear X. - simpl. - unfold is_true. - rewrite andb_true_iff. - split. - { - apply IHx1. apply X0. - } - { - apply IHx2. apply X1. - } - } - Qed. - Next Obligation. - simpl. - ltac1:(rename v into ρ). - ltac1:(rename a into x). - ltac1:(rename b into y). - revert y H. - induction x; intros y H; destruct y. - { - simpl in H. - apply bool_decide_eq_true in H. - subst. - constructor. - } - { - simpl in H. inversion H. - } - { - simpl in H. inversion H. - } - { - simpl in H. inversion H. - } - { - simpl in H. - unfold is_true in H. - rewrite andb_true_iff in H. - destruct H as [H1 H2]. - constructor; try ltac1:(naive_solver). - apply matchesb_satisfies in H2. - exact H2. - } - { - simpl in H. - unfold is_true in H. - rewrite andb_true_iff in H. - destruct H as [H1 H2]. - constructor; try ltac1:(naive_solver). - apply matchesb_satisfies in H2. - exact H2. - } - { - simpl in H. inversion H. - } - { - simpl in H. - unfold is_true in H. - rewrite andb_true_iff in H. - destruct H as [H1 H2]. - constructor; try ltac1:(naive_solver). - apply matchesb_satisfies in H2. - exact H2. - } - { - simpl in H. - unfold is_true in H. - rewrite andb_true_iff in H. - destruct H as [H1 H2]. - constructor; try ltac1:(naive_solver). - } - Qed. - Next Obligation. - revert b H. - unfold vars_of; simpl. - induction a; simpl; intros b' H. - { - destruct b'; simpl in *. - { ltac1:(set_solver). } - { inversion H. } - { inversion H. } - } - { - destruct b'. - { inversion H. } - { - rewrite andb_true_iff in H. - destruct H as [H1 H2]. - specialize (IHa b' H1). - apply matchesb_vars_of in H2. - clear -IHa H2. - ltac1:(set_solver). - } - { - rewrite andb_true_iff in H. - destruct H as [H1 H2]. - assert (IH1 := IHa b'1 H1). - apply matchesb_vars_of in H2. - clear -IH1 H2. - ltac1:(set_solver). - } - } - { - destruct b'. - { inversion H. } - { - rewrite andb_true_iff in H. - destruct H as [H1 H2]. - specialize (IHa1 b' H1). - apply matchesb_vars_of in H2. - clear -IHa1 H2. - ltac1:(set_solver). - } - { - rewrite andb_true_iff in H. - destruct H as [H1 H2]. - specialize (IHa1 b'1 H1). - specialize (IHa2 b'2 H2). - clear - IHa1 IHa2. - ltac1:(set_solver). - } - } - Qed. - Next Obligation. - revert b v1 v2 H. - induction a; intros b' v1 v2 H'; destruct b'; - simpl in *; - try reflexivity. - { - - unfold vars_of in H'; simpl in H'. - - erewrite IHa. - erewrite matchesb_insensitive. - reflexivity. - { - eapply valuation_restrict_eq_subseteq>[|apply H']. - clear. - ltac1:(set_solver). - } - { - eapply valuation_restrict_eq_subseteq>[|apply H']. - clear. - unfold vars_of at 1; simpl. - ltac1:(set_solver). - } - } - { - - unfold vars_of in H'; simpl in H'. - - erewrite IHa. - erewrite matchesb_insensitive. - reflexivity. - { - eapply valuation_restrict_eq_subseteq>[|apply H']. - clear. - ltac1:(set_solver). - } - { - eapply valuation_restrict_eq_subseteq>[|apply H']. - clear. - unfold vars_of at 1; simpl. - ltac1:(set_solver). - } - } - { - - unfold vars_of in H'; simpl in H'. - - erewrite IHa1. - erewrite matchesb_insensitive. - reflexivity. - { - eapply valuation_restrict_eq_subseteq>[|apply H']. - clear. - ltac1:(set_solver). - } - { - eapply valuation_restrict_eq_subseteq>[|apply H']. - clear. - unfold vars_of at 1; simpl. - ltac1:(set_solver). - } - } - { - - unfold vars_of in H'; simpl in H'. - - erewrite IHa1. - erewrite IHa2. - reflexivity. - { - eapply valuation_restrict_eq_subseteq>[|apply H']. - clear. - ltac1:(set_solver). - } - { - eapply valuation_restrict_eq_subseteq>[|apply H']. - clear. - unfold vars_of at 1; simpl. - ltac1:(set_solver). - } - } - Qed. - Fail Next Obligation. - - Definition ApppliedOperatorOr'_matches_Term' - {Operand1 Operand2 var : Type} - {_EDv : EqDecision var} - {_Cv : Countable var} - {_V1 : VarsOf Operand1 var} - {_V2 : VarsOf Operand2 var} - {_S1 : Satisfies (gmap var GroundTerm) (symbol) Operand2 var} - {_S2 : Satisfies (gmap var GroundTerm) (Operand1) Operand2 var} - {_S3 : Satisfies (gmap var GroundTerm) (Operand1) (PreTerm' symbol Operand2) var} - {_S4 : Satisfies (gmap var GroundTerm) ((PreTerm' symbol Operand1)) Operand2 var} - {_M1 : Matches (symbol) Operand2 var} - {_M2 : Matches (Operand1) Operand2 var} - {_M3 : Matches (Operand1) (PreTerm' symbol Operand2) var} - {_M4 : Matches ((PreTerm' symbol Operand1)) Operand2 var} - (ρ : (gmap var GroundTerm)) - (x : (Term' symbol Operand1)) - (y : Term' symbol Operand2) - : bool := - match x, y with - | term_preterm app1, term_preterm app2 => - matchesb ρ app1 app2 - | term_preterm app1, term_operand o2 => - matchesb ρ app1 o2 - | term_operand o1, term_preterm app2 => - false (*matchesb (ρ, o1) app2*) - | term_operand o1, term_operand o2 => - matchesb ρ o1 o2 - end. - - #[export] - Program Instance - reflect__satisfies__ApppliedOperatorOr'_matches_Term' - {Operand1 Operand2 var : Type} - {_EDv : EqDecision var} - {_Cv : Countable var} - {_V1 : VarsOf Operand1 var} - {_V2 : VarsOf Operand2 var} - {_S1 : Satisfies (gmap var GroundTerm) (symbol) Operand2 var} - {_S2 : Satisfies (gmap var GroundTerm) (Operand1) Operand2 var} - {_S3 : Satisfies (gmap var GroundTerm) (Operand1) (PreTerm' symbol Operand2) var} - {_S4 : Satisfies (gmap var GroundTerm) ((PreTerm' symbol Operand1)) Operand2 var} - {_M1 : Matches (symbol) Operand2 var} - {_M2 : Matches (Operand1) Operand2 var} - {_M3 : Matches (Operand1) (PreTerm' symbol Operand2) var} - {_M4 : Matches ((PreTerm' symbol Operand1)) Operand2 var} - : - Matches - (Term' symbol Operand1) - (Term' symbol Operand2) - var - := {| - matchesb := - ApppliedOperatorOr'_matches_Term'; - matchesb_satisfies := _; - |}. - Next Obligation. - destruct a,b; simpl. - { - inversion X; subst; clear X. - apply satisfies_matchesb. - assumption. - } - { - inversion X; subst; clear X. - apply satisfies_matchesb. - assumption. - } - { - inversion X. - } - { - inversion X; subst; clear X. - apply satisfies_matchesb. - assumption. - } - Qed. - Next Obligation. - destruct a,b; simpl in H. - { - constructor. apply matchesb_satisfies. assumption. - } - { - constructor. apply matchesb_satisfies. assumption. - } - { - inversion H. - } - { - constructor. apply matchesb_satisfies. assumption. - } - Qed. - Next Obligation. - destruct a,b; simpl in *. - { - apply matchesb_vars_of in H. - assumption. - } - { - apply matchesb_vars_of in H. - assumption. - } - { inversion H. } - { - apply matchesb_vars_of in H. - assumption. - } - Qed. - Next Obligation. - destruct a,b; unfold vars_of in H; simpl in *. - { - apply matchesb_insensitive. - apply H. - } - { - apply matchesb_insensitive. - apply H. - } - { reflexivity. } - { - apply matchesb_insensitive. - apply H. - } - Qed. - Fail Next Obligation. - - Definition builtin_value_matches_BuiltinOrVar - : Valuation -> builtin_value -> BuiltinOrVar -> bool := - fun ρ b bv => - match bv with - | bov_builtin b' => bool_decide (b = b') - | bov_variable x => - match ρ !! x with - | None => false - | Some (term_preterm _) => false - | Some (term_operand b') => bool_decide (b = b') - end - end. - - #[export] - Program Instance - reflect__matches__builtin_value__BuiltinOrVar - : - Matches - (builtin_value) - BuiltinOrVar - variable - := {| - matchesb := - builtin_value_matches_BuiltinOrVar; - matchesb_satisfies := _; - |}. - Next Obligation. - destruct b; simpl. - { - inversion X; subst; clear X. - unfold is_true. - rewrite bool_decide_eq_true. - reflexivity. - } - { - inversion X; subst; clear X. - rewrite H1. - unfold is_true. - rewrite bool_decide_eq_true. - reflexivity. - } - Qed. - Next Obligation. - destruct b; simpl in H. - { - unfold is_true in H. - rewrite bool_decide_eq_true in H. - subst. - constructor. - } - { - unfold Valuation in *. - destruct (v !! x) eqn:Hvx. - { - destruct t. - { - inversion H. - } - { - unfold is_true in H. - rewrite bool_decide_eq_true in H. - subst a. - constructor. - exact Hvx. - } - } - { - inversion H. - } - } - Qed. - Next Obligation. - unfold vars_of; destruct b; simpl. - { ltac1:(clear; set_solver). } - { - simpl in H. - unfold Valuation in *. - destruct (v !! x) as [a0|] eqn:Hvx. - { - rewrite elem_of_subseteq. - intros x0 Hx0. - rewrite elem_of_singleton in Hx0. - subst. - rewrite elem_of_dom. - exists a0. assumption. - } - { - inversion H. - } - } - Qed. - Next Obligation. - destruct b; unfold vars_of in H; simpl in *. - { - reflexivity. - } - { - unfold valuation_restrict in H. - rewrite map_eq_iff in H. - specialize (H x). - rewrite map_lookup_filter in H. - rewrite map_lookup_filter in H. - ltac1:(repeat case_match); try reflexivity; - subst. - { - symmetry. apply bool_decide_eq_false. - intros HContra. subst. - - unfold Valuation in *. - ltac1:(rewrite H0 in H). - ltac1:(rewrite H2 in H). - simpl in H. - ltac1:(repeat case_guard; simpl in *; simplify_eq/=; set_solver). - } - { - apply bool_decide_eq_false. - intros HContra. subst. - - unfold Valuation in *. - ltac1:(rewrite H0 in H). - ltac1:(rewrite H2 in H). - simpl in H. - ltac1:(repeat case_guard; simpl in *; simplify_eq/=; set_solver). - } - { - unfold bool_decide. - unfold Valuation in *. - ltac1:(rewrite H0 in H). - ltac1:(rewrite H2 in H). - simpl in H. - ltac1:(repeat case_guard; simpl in *; simplify_eq/=; set_solver). - } - { - apply bool_decide_eq_false. - intros HContra. - subst. - - unfold Valuation in *. - ltac1:(rewrite H0 in H). - ltac1:(rewrite H2 in H). - simpl in H. - ltac1:(repeat case_guard; simpl in *; simplify_eq/=; set_solver). - } - { - symmetry. - apply bool_decide_eq_false. - intros HContra. - subst. - - unfold Valuation in *. - ltac1:(rewrite H0 in H). - ltac1:(rewrite H1 in H). - simpl in H. - ltac1:(repeat case_guard; simpl in *; simplify_eq/=; set_solver). - } - } - Qed. - Fail Next Obligation. - - (* Can this be simplified? *) - Definition builtin_value_matches_SymbolicTerm - : Valuation -> builtin_value -> SymbolicTerm -> bool := - fun ρ b t => - match t with - | term_preterm _ => false - | term_operand (bov_variable x) => - match ρ !! x with - | None => false - | Some (term_preterm _) => false - | Some (term_operand b') => bool_decide (b = b') - end - | term_operand (bov_builtin b') => - bool_decide (b = b') - end. - - #[export] - Program Instance - reflect__matches__builtin_value__SymbolicTerm - : - Matches - (builtin_value) - SymbolicTerm - variable - := {| - matchesb := builtin_value_matches_SymbolicTerm; - matchesb_satisfies := _; - |}. - Next Obligation. - destruct b; simpl in *. - { - inversion X. - } - { - destruct operand. - { - inversion X; subst; clear X. - unfold is_true. - rewrite bool_decide_eq_true. - reflexivity. - } - { - inversion X; subst; clear X. - rewrite H1. - unfold is_true. - rewrite bool_decide_eq_true. - reflexivity. - } - } - Qed. - Next Obligation. - destruct b; simpl in *. - { inversion H. } - { - destruct operand. - { - unfold is_true in H. - rewrite bool_decide_eq_true in H. - subst. - constructor. - } - { - unfold Valuation in *. - destruct (v !! x) eqn:Hvx. - { - destruct t. - { - inversion H. - } - { - unfold is_true in H. - rewrite bool_decide_eq_true in H. - subst. - constructor. - exact Hvx. - } - } - { - inversion H. - } - } - } - Qed. - Next Obligation. - destruct b; unfold vars_of at 1; simpl in *. - { - inversion H. - } - { - ltac1:(repeat case_match); subst; unfold vars_of; simpl. - { ltac1:(set_solver). } - { inversion H. } - { - rewrite elem_of_subseteq. - intros x0 Hx0. - rewrite elem_of_singleton in Hx0. - subst. - unfold Valuation in *. - rewrite elem_of_dom. - eexists. ltac1:(eassumption). - } - { inversion H. } - } - Qed. - Next Obligation. - destruct b; simpl in *. - { reflexivity. } - - unfold vars_of in *; simpl in *. - unfold vars_of in *; simpl in *. - ltac1:(repeat case_match); - try reflexivity. - { - symmetry. - apply bool_decide_eq_false. - intros HContra. - subst. - simpl in *. - apply valuation_restrict_eq_impl_lookup with (x := x) in H. - { - ltac1:(rewrite H in H1). - ltac1:(rewrite H3 in H1). - ltac1:(congruence). - } - { - ltac1:(set_solver). - } - } - { - subst. - apply bool_decide_eq_false. - intros HContra. - subst. - simpl in *. - apply valuation_restrict_eq_impl_lookup with (x := x) in H. - { - ltac1:(rewrite H in H1). - ltac1:(rewrite H3 in H1). - ltac1:(congruence). - } - { - ltac1:(set_solver). - } - } - { - subst. - simpl in *. - apply valuation_restrict_eq_impl_lookup with (x := x) in H. - { - ltac1:(rewrite H in H1). - ltac1:(rewrite H3 in H1). - inversion H1; subst; clear H1. - ltac1:(congruence). - } - { - ltac1:(set_solver). - } - } - { - subst. - apply bool_decide_eq_false. - intros HContra. - subst. - simpl in *. - apply valuation_restrict_eq_impl_lookup with (x := x) in H. - { - ltac1:(rewrite H in H1). - ltac1:(rewrite H3 in H1). - ltac1:(congruence). - } - { - ltac1:(set_solver). - } - } - { - subst. - symmetry. - apply bool_decide_eq_false. - intros HContra. - subst. - simpl in *. - apply valuation_restrict_eq_impl_lookup with (x := x) in H. - { - ltac1:(rewrite H in H1). - ltac1:(rewrite H1 in H2). - ltac1:(congruence). - } - { - ltac1:(set_solver). - } - } - Qed. - Fail Next Obligation. - - Definition Term'_matches_BuiltinOrVar - : Valuation -> (PreTerm' symbol builtin_value) -> - BuiltinOrVar -> - bool - := fun ρ t bov => - match bov with - | bov_builtin b => false - | bov_variable x => - bool_decide (ρ !! x = Some (term_preterm t)) - end. - - #[export] - Program Instance - matches__builtin_value__SymbolicTerm - : - Matches - (PreTerm' symbol builtin_value) - BuiltinOrVar - variable - := {| - matchesb := Term'_matches_BuiltinOrVar; - matchesb_satisfies := _; - |}. - Next Obligation. - destruct b; simpl in *. - { - inversion X. - } - { - inversion X; subst; clear X. - unfold is_true. - rewrite bool_decide_eq_true. - reflexivity. - } - Qed. - Next Obligation. - destruct b; simpl in *. - { inversion H. } - { - unfold satisfies; simpl. - unfold is_true in H. - rewrite bool_decide_eq_true in H. - apply H. - } - Qed. - Next Obligation. - destruct b; simpl in *. - { inversion H. } - { - rewrite bool_decide_eq_true in H. - unfold vars_of; simpl. - rewrite elem_of_subseteq. - intros x0 Hx0. - rewrite elem_of_singleton in Hx0. - subst. - unfold Valuation in *. - rewrite elem_of_dom. - eexists. ltac1:(eassumption). - } - Qed. - Next Obligation. - destruct b; simpl in *. - { reflexivity. } - unfold bool_decide. - ltac1:(repeat case_match); try reflexivity. - { - clear H0 H1. - ltac1:(exfalso). - apply n. - eapply valuation_restrict_eq_impl_lookup in H. - { - rewrite H in e. - ltac1:(rewrite e in n). - ltac1:(contradiction). - } - { - unfold vars_of; simpl. - rewrite elem_of_singleton. - reflexivity. - } - } - { - eapply valuation_restrict_eq_impl_lookup in H. - { - clear H0 H1. - rewrite H in n. - ltac1:(rewrite e in n). - ltac1:(contradiction). - } - { - unfold vars_of; simpl. - rewrite elem_of_singleton. - reflexivity. - } - } - Qed. - Fail Next Obligation. - - #[export] - Program Instance Matches_bv_ao' - {B var : Type} - {_EDv : EqDecision var} - {_Cv : Countable var} - {_VB : VarsOf B var} - : - Matches - builtin_value - (PreTerm' symbol B) - var - := {| - matchesb := fun _ _ _ => false ; - |}. - Fail Next Obligation. - - #[export] - Instance VarsOf_LeftRight - {_VO : VarsOf Valuation (LeftRight * variable)} - : - VarsOf (Valuation * LeftRight) variable - := {| - vars_of := fun ρd => - let ρ := ρd.1 in - let d := ρd.2 in - let vs : gset (LeftRight * variable) := vars_of ρ in - let vs' := filter (fun x => x.1 = d) vs in - set_map (fun x : LeftRight * variable => x.2) vs' - |}. - - (* - #[export] - Program Instance Matches_vlrblrootob - : - Matches - (Valuation * LeftRight) - (builtin_value) - (PreTerm' symbol LocalRewriteOrSymbolicTermOrBOV) - (variable) - := {| - matchesb := fun _ _ _ => false ; - |}. - Next Obligation. - unfold satisfies; simpl. - apply ReflectF. ltac1:(tauto). - Qed. - Fail Next Obligation. - *) - - - #[export] - Program Instance - Matches_symbol_B - {B var : Type} - {_VarED : EqDecision var} - {_VarCnt : Countable var} - {_VB : VarsOf B var} - : - Matches symbol B var - := {| - matchesb := fun _ _ _ => false - |}. - Fail Next Obligation. - - #[export] - Instance - matches__GroundTerm__SymbolicTerm - : - Matches - GroundTerm - SymbolicTerm - variable - . - Proof. - unfold GroundTerm. - unfold SymbolicTerm. - ltac1:(unshelve(eapply reflect__satisfies__ApppliedOperatorOr'_matches_Term')). - Defined. - -End with_signature. - -Definition val_satisfies_ap_bool - {Σ : StaticModel} - - (ρ : Valuation) - (ap : AtomicProposition) - : bool := -match ap with -| apeq e1 e2 => - let v1 := Expression_evaluate ρ e1 in - let v2 := Expression_evaluate ρ e2 in - bool_decide (v1 = v2) && isSome v1 -end -. - -Lemma expression_evaluate_some_valuation - {Σ : StaticModel} ρ e x - : - Expression_evaluate ρ e = Some x -> - vars_of e ⊆ vars_of ρ. -Proof. - revert x. - induction e; unfold vars_of; simpl; intros x' H. - { - ltac1:(set_solver). - } - { - rewrite elem_of_subseteq. - intros x1 Hx1. - rewrite elem_of_singleton in Hx1. - subst. - unfold Valuation in *. - rewrite elem_of_dom. - exists x'. assumption. - } - { - ltac1:(set_solver). - } - { - rewrite bind_Some in H. - destruct H as [x0 [H1x0 H2x0]]. - inversion H2x0; subst; clear H2x0. - rewrite fmap_Some in H1x0. - destruct H1x0 as [x1 [H1x1 H2x1]]. - subst x0. - ltac1:(naive_solver). - } - { - rewrite bind_Some in H. - destruct H as [x0 [H1x0 H2x0]]. - inversion H2x0; subst; clear H2x0. - - rewrite bind_Some in H0. - destruct H0 as [x1 [H1x1 H2x1]]. - inversion H2x1; subst; clear H2x1. - rewrite fmap_Some in H1x0. - rewrite fmap_Some in H1x1. - destruct H1x0 as [y [H1y H2y]]. - destruct H1x1 as [z [H1z H2z]]. - subst. - ltac1:(set_solver). - } - { - rewrite bind_Some in H. - destruct H as [x0 [H1x0 H2x0]]. - inversion H2x0; subst; clear H2x0. - - rewrite bind_Some in H0. - destruct H0 as [x1 [H1x1 H2x1]]. - inversion H2x1; subst; clear H2x1. - - rewrite bind_Some in H0. - destruct H0 as [x2 [H1x2 H2x2]]. - inversion H2x2; subst; clear H2x2. - - rewrite fmap_Some in H1x0. - rewrite fmap_Some in H1x1. - rewrite fmap_Some in H1x2. - destruct H1x0 as [y [H1y H2y]]. - destruct H1x1 as [z [H1z H2z]]. - destruct H1x2 as [t [H1t H2t]]. - subst. - ltac1:(set_solver). - } -Qed. - -Lemma Expression_evaluate_val_restrict: - ∀ {Σ : StaticModel} - (ρ1 ρ2 : gmap variable GroundTerm) - (t : Expression), - valuation_restrict ρ1 (vars_of t) = valuation_restrict ρ2 (vars_of t) → - Expression_evaluate ρ1 t = Expression_evaluate ρ2 t -. -Proof. - intros Σ ρ1 ρ2 t. - revert ρ1 ρ2. - induction t; intros ρ1 ρ2; unfold vars_of in *; simpl in *. - { solve[auto]. } - { - intros H1. - unfold is_true, isSome in *. - unfold valuation_restrict in H1. - rewrite map_eq_iff in H1. - specialize (H1 x). - do 2 (rewrite map_lookup_filter in H1). - destruct (ρ1!!x),(ρ2!!x); simpl in *; try reflexivity. - { - ltac1:(repeat case_guard; simpl in *; simplify_eq/=; set_solver). - } - { - ltac1:(repeat case_guard; simpl in *; simplify_eq/=; set_solver). - } - { - ltac1:(repeat case_guard; simpl in *; simplify_eq/=; set_solver). - } - } - { - intros ?. reflexivity. - } - { - intros H1. - specialize (IHt _ _ H1). - rewrite IHt. - reflexivity. - } - { - intros H1. - assert (H2 : valuation_restrict ρ1 (vars_of_Expression t1) = valuation_restrict ρ2 (vars_of_Expression t1)). - { - eapply valuation_restrict_eq_subseteq>[|apply H1]. - ltac1:(set_solver). - } - assert (H3 : valuation_restrict ρ1 (vars_of_Expression t2) = valuation_restrict ρ2 (vars_of_Expression t2)). - { - eapply valuation_restrict_eq_subseteq>[|apply H1]. - ltac1:(set_solver). - } - specialize (IHt1 _ _ H2). - specialize (IHt2 _ _ H3). - rewrite IHt1. - rewrite IHt2. - reflexivity. - } - { - intros H1. - assert (H2 : valuation_restrict ρ1 (vars_of_Expression t1) = valuation_restrict ρ2 (vars_of_Expression t1)). - { - eapply valuation_restrict_eq_subseteq>[|apply H1]. - ltac1:(set_solver). - } - assert (H3 : valuation_restrict ρ1 (vars_of_Expression t2) = valuation_restrict ρ2 (vars_of_Expression t2)). - { - eapply valuation_restrict_eq_subseteq>[|apply H1]. - ltac1:(set_solver). - } - assert (H4 : valuation_restrict ρ1 (vars_of_Expression t3) = valuation_restrict ρ2 (vars_of_Expression t3)). - { - eapply valuation_restrict_eq_subseteq>[|apply H1]. - ltac1:(set_solver). - } - specialize (IHt1 _ _ H2). - specialize (IHt2 _ _ H3). - specialize (IHt3 _ _ H4). - rewrite IHt1. - rewrite IHt2. - rewrite IHt3. - reflexivity. - } -Qed. - -#[export] -Program Instance Matches_val_ap - {Σ : StaticModel} - - : Matches unit AtomicProposition variable -:= {| - matchesb := fun a b c => val_satisfies_ap_bool a c; -|}. -Next Obligation. - destruct b. - unfold satisfies in X; simpl in X. - destruct X as [H1 H2]. - unfold val_satisfies_ap_bool. - unfold is_true. - rewrite andb_true_iff. - rewrite bool_decide_eq_true. - split>[exact H1|]. - unfold isSome in H2. - destruct (Expression_evaluate v e1) eqn:H2'>[|inversion H2]. - unfold isSome. - reflexivity. -Qed. -Next Obligation. - destruct b; simpl in *. - unfold is_true in H. - rewrite andb_true_iff in H. - destruct H as [H1 H2]. - rewrite bool_decide_eq_true in H1. - constructor. - { exact H1. } - { - unfold isSome in H2. - unfold is_Some. - destruct (Expression_evaluate v e1). - { reflexivity. } - { inversion H2. } - } -Qed. -Next Obligation. - destruct b; unfold vars_of in *; simpl in *. - { - rewrite andb_true_iff in H. - rewrite bool_decide_eq_true in H. - destruct H as [H1 H2]. - unfold isSome in *. - destruct (Expression_evaluate v e1) eqn:Heq2>[|inversion H2]. - clear H2. symmetry in H1. - unfold vars_of. simpl. - apply expression_evaluate_some_valuation in Heq2. - apply expression_evaluate_some_valuation in H1. - rewrite union_subseteq. - split; assumption. - } -Qed. -Next Obligation. - revert v1 v2 H. - induction b; intros v1 v2 HH; simpl in *. - { - unfold vars_of in HH; simpl in *. - rewrite Expression_evaluate_val_restrict with (ρ1 := v1) (ρ2 := v2). - rewrite Expression_evaluate_val_restrict with (ρ1 := v1) (ρ2 := v2). - reflexivity. - { - eapply valuation_restrict_eq_subseteq>[|apply HH]. - ltac1:(set_solver). - } - { - eapply valuation_restrict_eq_subseteq>[|apply HH]. - ltac1:(set_solver). - } - } -Qed. -Fail Next Obligation. - - -Definition valuation_satisfies_sc_bool - {Σ : StaticModel} - - (ρ : Valuation) - (sc : SideCondition) : bool := -match sc with -| sc_constraint c => matchesb ρ () c -end. - -#[export] -Program Instance Matches_valuation_sc - {Σ : StaticModel} - - : - Matches unit SideCondition variable -:= {| - matchesb := fun a b c => valuation_satisfies_sc_bool a c; -|}. -Next Obligation. - destruct b; simpl in *. - unfold satisfies in X; simpl in X. - apply satisfies_matchesb. - assumption. -Qed. -Next Obligation. - destruct b; simpl in *. - apply matchesb_satisfies in H. - apply H. -Qed. -Next Obligation. - destruct b; unfold vars_of; simpl in *. - { - apply matchesb_vars_of in H. - exact H. - } -Qed. -Next Obligation. - destruct b; unfold vars_of in H; simpl in *. - { - apply matchesb_insensitive. - exact H. - } -Qed. -Fail Next Obligation. - -#[export] -Program Instance Matches_valuation_scs - {Σ : StaticModel} - : - Matches unit (list SideCondition) variable -:= {| - matchesb := fun ρ b c => forallb (matchesb ρ ()) c; -|}. -Next Obligation. - unfold satisfies in X; simpl in X. - unfold is_true. - rewrite forallb_forall. - intros x Hx. - rewrite <- elem_of_list_In in Hx. - specialize (X x Hx). - apply satisfies_matchesb. - assumption. -Qed. -Next Obligation. - unfold is_true in H. - rewrite forallb_forall in H. - unfold satisfies; simpl. - intros x Hx. - rewrite elem_of_list_In in Hx. - specialize (H x Hx). - apply matchesb_satisfies. - assumption. -Qed. -Next Obligation. - unfold vars_of; simpl. - rewrite forallb_forall in H. - rewrite elem_of_subseteq. - intros x Hx. - rewrite elem_of_union_list in Hx. - destruct Hx as [X [H1X H2X]]. - unfold Valuation in *. - rewrite elem_of_list_fmap in H1X. - destruct H1X as [y [H1y H2y]]. - subst. - - specialize (H y). - rewrite <- elem_of_list_In in H. - specialize (H ltac:(assumption)). - apply matchesb_vars_of in H. - - rewrite elem_of_subseteq in H. - specialize (H x H2X). - exact H. -Qed. -Next Obligation. - revert H. - induction b; simpl; intros HH. - { reflexivity. } - { - unfold vars_of in HH; simpl in HH. - ltac1:(ospecialize (IHb _)). - { - eapply valuation_restrict_eq_subseteq>[|apply HH]. - unfold vars_of at 1; simpl. - unfold fmap; simpl. - ltac1:(set_solver). - } - rewrite IHb. - erewrite matchesb_insensitive. - reflexivity. - eapply valuation_restrict_eq_subseteq>[|apply HH]. - ltac1:(set_solver). - } -Qed. -Fail Next Obligation. - - - -#[export] -Program Instance Matches__builtin__Expr - {Σ : StaticModel} - - : - Matches builtin_value (Expression) variable -:= {| - matchesb := (fun ρ b e => - bool_decide (Expression_evaluate ρ e = Some (term_operand b)) - ) ; -|}. -Next Obligation. - unfold satisfies. simpl. - unfold is_true. - rewrite bool_decide_eq_true. - unfold satisfies in X; simpl in X. - exact X. -Qed. -Next Obligation. - unfold is_true in H. - rewrite bool_decide_eq_true in H. - apply H. -Qed. -Next Obligation. - apply bool_decide_eq_true in H. - apply expression_evaluate_some_valuation in H. - assumption. -Qed. -Next Obligation. - erewrite Expression_evaluate_val_restrict. - reflexivity. - exact H. -Qed. -Fail Next Obligation. - -#[export] -Program Instance Matches_asb_expr - {Σ : StaticModel}: - Matches - ((PreTerm' symbol builtin_value)) - Expression - variable -:= {| - matchesb := (fun ρ x e => - bool_decide (Expression_evaluate ρ e = Some (term_preterm x)) ) ; -|}. -Next Obligation. - unfold is_true. - rewrite bool_decide_eq_true. - apply X. -Qed. -Next Obligation. - unfold is_true in H. - rewrite bool_decide_eq_true in H. - apply H. -Qed. -Next Obligation. - apply bool_decide_eq_true in H. - apply expression_evaluate_some_valuation in H. - assumption. -Qed. -Next Obligation. - erewrite Expression_evaluate_val_restrict. - reflexivity. - exact H. -Qed. -Fail Next Obligation. - diff --git a/minuska/theories/minusl_compile_properties.v b/minuska/theories/minusl_compile_properties.v index 2081bb1e..70a9b3ea 100644 --- a/minuska/theories/minusl_compile_properties.v +++ b/minuska/theories/minusl_compile_properties.v @@ -5,7 +5,6 @@ From Minuska Require Import lowlang properties semantics_properties - basic_matching varsof syntax_properties minusl_compile @@ -2227,155 +2226,6 @@ Proof. } Qed. -Lemma satisfies_PreTerm'_vars_of_1 - {Σ : StaticModel} - (ρ1 ρ2 : Valuation) - (g : PreTerm' symbol builtin_value) - (φ : PreTerm' symbol BuiltinOrVar) -: - (forall (x : variable), x ∈ vars_of φ -> ρ1!!x = ρ2!!x) -> - ( - satisfies ρ1 g φ - -> - satisfies ρ2 g φ - ) -. -Proof. - unfold Valuation in *. - intros H1 H2. - apply satisfies_matchesb in H2. - apply matchesb_satisfies. - revert H1 H2. - revert φ. - induction g; intros φ Hvars; destruct φ; - unfold matchesb in *; unfold vars_of in *; - simpl in *; - try ltac1:(tauto). - { - unfold is_true. - do 2 (rewrite andb_true_iff). - intros [HH1 HH2]. - split. - { - apply IHg>[|assumption]. - ltac1:(set_solver). - } - { - unfold matchesb in HH2; simpl in HH2. - unfold matchesb; simpl. - destruct b0; simpl in *. - { apply HH2. } - rewrite Hvars in HH2. - apply HH2. - unfold vars_of; simpl. - ltac1:(set_solver). - } - } - { - do 2 (rewrite andb_true_iff). - intros [HH1 HH2]. - split. - { - apply IHg>[|assumption]. - ltac1:(set_solver). - } - { - unfold matchesb in HH2; simpl in HH2. - unfold matchesb; simpl. - apply HH2. - } - } - { - unfold is_true. - do 2 (rewrite andb_true_iff). - intros [HH1 HH2]. - split. - { - apply IHg1>[|assumption]. - ltac1:(set_solver). - } - { - unfold matchesb in HH2; simpl in HH2. - unfold matchesb; simpl. - destruct b; simpl in *. - { inversion HH2. } - { - rewrite Hvars in HH2. - apply HH2. - unfold vars_of; simpl. - ltac1:(set_solver). - } - } - } - { - do 2 (rewrite andb_true_iff). - intros [HH1 HH2]. - split; ltac1:(set_solver). - } -Qed. - -Lemma satisfies_Term'_vars_of_1 - {Σ : StaticModel} - (ρ1 ρ2 : Valuation) - (g : Term' symbol builtin_value) - (φ : Term' symbol BuiltinOrVar) -: - (forall (x : variable), x ∈ vars_of φ -> ρ1!!x = ρ2!!x) -> - ( - satisfies ρ1 g φ - -> - satisfies ρ2 g φ - ) -. -Proof. - intros H1 H2. - apply matchesb_satisfies. - apply satisfies_matchesb in H2. - revert H1 H2. - intros Hvars. - destruct g, φ; unfold matchesb; simpl. - { - intros HH1. - apply matchesb_satisfies in HH1. - apply satisfies_matchesb. - eapply satisfies_PreTerm'_vars_of_1>[|apply HH1]. - apply Hvars. - } - { - unfold matchesb; simpl. - destruct operand; simpl. - { ltac1:(tauto). } - { - rewrite Hvars. - { ltac1:(tauto). } - { - unfold vars_of; simpl. - unfold vars_of; simpl. - rewrite elem_of_singleton. - reflexivity. - } - } - } - { - ltac1:(tauto). - } - { - unfold matchesb; simpl. - destruct operand0; simpl. - { ltac1:(tauto). } - { - rewrite Hvars. - { ltac1:(tauto). } - { - unfold vars_of; simpl. - unfold vars_of; simpl. - rewrite elem_of_singleton. - reflexivity. - } - } - } -Qed. - Lemma vars_of_uglify {Σ : StaticModel} (h : variable) a: @@ -2439,39 +2289,6 @@ Qed. -Fixpoint factor_by_subst - {Σ : StaticModel} - (sz : nat) - (ρ : Valuation) - (h : variable) - (γ : TermOver builtin_value) - (φ ψ : TermOver BuiltinOrVar) - : ((TermOver builtin_value)*(TermOver builtin_value)) -:= -match sz with -| 0 => (γ, γ) -| S sz' => - if matchesb ρ (uglify' γ) (uglify' ψ) then (γ, γ) else - match γ,φ with - | t_over _, t_over _ => (* do not care*) (γ, γ) - | t_term _ _, t_over _ => (* do not care*) (γ, γ) - | t_over _, t_term _ _ => (* do not care*) (γ, γ) - | t_term _ lγ, t_term s lφ => - match list_find (fun φi => h ∈ vars_of_to_l2r φi) lφ with - | None => (* do not care*) (γ, γ) - | Some (i, φi) => - match lγ !! i with - | None => (* do not care*) (γ, γ) - | Some γi => - let xy := factor_by_subst sz' ρ h γi φi ψ in - (t_term s (<[i := xy.1]>lγ), xy.2) - - end - end - end -end -. - Lemma length_filter_l_1_impl_h_in_l {Σ : StaticModel} (l : list variable) @@ -5733,1359 +5550,154 @@ Proof. } Qed. -(* -(* TODO we need a lemma like this that does not assume h ∉ ρ. - Instead of the uses of that assumption for satisfies_ext, - we have to use the `vars_of` lemmas about `satisfies`, - and it should still work. -*) -Lemma factor_by_subst_correct' + +Lemma frto_step_app {Σ : StaticModel} - (sz : nat) - (ρ : Valuation) - (h : variable) - (γ : TermOver builtin_value) - (φ ψ : TermOver BuiltinOrVar) - : sz >= TermOver_size γ -> - h ∉ vars_of ρ -> - length (filter (eq h) (vars_of_to_l2r φ)) = 1 -> - ~ (h ∈ vars_of_to_l2r ψ) -> - satisfies ρ γ (TermOverBoV_subst φ h ψ) -> - let xy := factor_by_subst sz ρ h γ φ ψ in - satisfies ρ xy.2 ψ /\ - satisfies (<[h := (uglify' xy.2)]>ρ) xy.1 φ + (Act : Set) + : + forall + Γ + (t1 t2 t3 : TermOver builtin_value) + (w : list Act) + (a : Act) + r, + r ∈ Γ -> + flattened_rewrites_to_over Γ t1 w t2 -> + flattened_rewrites_to r (uglify' t2) a (uglify' t3) -> + flattened_rewrites_to_over Γ t1 (w++[a]) t3 +. +Proof. + intros Γ t1 t2 t3 w a r Hr H1 H2. + induction H1. + { + simpl. + eapply frto_step. + { exact Hr. } + { exact H2. } + { apply frto_base. } + } + { + simpl. + specialize (IHflattened_rewrites_to_over H2). + eapply frto_step. + { exact e. } + { exact f. } + { apply IHflattened_rewrites_to_over. } + } +Qed. + + +Lemma frto_app + {Σ : StaticModel} + (Act : Set) + : + forall + Γ + (t1 t2 t3 : TermOver builtin_value) + (w1 w2 : list Act), + flattened_rewrites_to_over Γ t1 w1 t2 -> + flattened_rewrites_to_over Γ t2 w2 t3 -> + flattened_rewrites_to_over Γ t1 (w1++w2) t3 . Proof. - revert γ φ. - induction sz; intros γ φ Hsz. + intros. + revert t1 t2 t3 w2 X X0. + induction w1; intros t1 t2 t3 w2 H0 H1. { - destruct γ; simpl in Hsz; ltac1:(lia). + inversion H0; subst; clear H0. + simpl. + exact H1. } { - intros Hnotinρ Hlf Hnotinψ Hsat. - unfold factor_by_subst. fold (@factor_by_subst Σ). simpl. - destruct (matchesb ρ (uglify' γ) (uglify' ψ)) eqn:Heqmb. + inversion H0; subst; clear H0. + eapply frto_step>[|apply X|]. + { assumption. } { - simpl. - split. - { - apply matchesb_implies_satisfies in Heqmb. - unfold satisfies; simpl. - apply Heqmb. - } - { - apply matchesb_implies_satisfies in Heqmb. - assert (Heqmb': satisfies ρ γ ψ). - { - unfold satisfies; simpl. - apply Heqmb. - } + eapply IHw1. + { apply X0. } + { apply H1. } + } + } +Qed. - assert (Htmp2 := TermOver_size_not_zero ψ). - assert (Htmp3 := TermOver_size_not_zero φ). - assert (Hsat' := Hsat). - apply concrete_is_larger_than_symbolic in Hsat'. - apply concrete_is_larger_than_symbolic in Heqmb'. - unfold delta_in_val in Hsat'. - assert (Hperm := vars_of_to_l2r_subst φ ψ h Hlf Hnotinψ). - apply sum_list_with_perm with (f := (size_of_var_in_val ρ)) in Hperm. - rewrite Hperm in Hsat'. clear Hperm. - rewrite TermOverBoV_subst_once_size in Hsat'. - { +Lemma val_elem_of_dom_1 + {Σ : StaticModel} + (ρ : gmap variable GroundTerm) + (x : variable) + : + x ∈ dom ρ -> isSome (ρ !! x) = true +. +Proof. + rewrite elem_of_dom. + destruct (ρ!!x); simpl. + { + intros _. reflexivity. + } + { + intros H. unfold is_Some in H. + destruct H as [x0 Hx0]. + inversion Hx0. + } +Qed. - rewrite sum_list_with_app in Hsat'. - unfold delta_in_val in Heqmb'. - assert (Hszφ: TermOver_size φ = 1) by ltac1:(lia). - clear Hsat. - destruct φ. - { - simpl in *. clear Hszφ. - clear Htmp3. - destruct a. - { - simpl in *. ltac1:(lia). - } - simpl in *. rewrite filter_cons in Hlf. - destruct (decide (h = x)). - { - subst. - clear Heqmb' Hsat' Htmp2. clear Hlf. - simpl. - apply satisfies_var. - unfold Valuation in *. - apply lookup_insert. - } - { - simpl in *. ltac1:(lia). - } - } - { - simpl in Hszφ. - destruct l. - { - simpl in *. clear Hszφ Htmp3 Heqmb' Hsat'. - ltac1:(lia). - } - { - simpl in *. - ltac1:(lia). - } - } - } + +Lemma satisfies_TermOverBoV_to_TermOverExpr + {Σ : StaticModel} + (ρ : Valuation) + (γ : TermOver builtin_value) + (φ : TermOver BuiltinOrVar) + : + satisfies ρ γ (TermOverBoV_to_TermOverExpr φ) + -> + satisfies ρ γ φ +. +Proof. + revert γ. + ltac1:(induction φ using TermOver_rect); intros γ. + { + unfold TermOverBoV_to_TermOverExpr. + simpl. + intros H. + { + destruct a; simpl in *. + { + inversion H; subst; clear H. + { + apply (f_equal prettify) in H2. + rewrite (cancel prettify uglify') in H2. + subst γ. + constructor. + inversion pf; subst; clear pf. + constructor. + } + { + apply (f_equal prettify) in H2. + rewrite (cancel prettify uglify') in H2. + subst γ. + inversion X. + } + } + { + inversion H; subst; clear H. { - rewrite <- vars_of_uglify. + apply (f_equal prettify) in H2. + rewrite (cancel prettify uglify') in H2. + subst γ. + constructor. + inversion pf; subst; clear pf. + constructor. assumption. } { - assumption. - } - } - } - { - destruct γ. - { - destruct φ. - { - destruct a0; simpl in *. - { - ltac1:(lia). - } - { - rewrite filter_cons in Hlf. - destruct (decide (h = x)). - { - subst. simpl in *. clear Hlf. - split>[exact Hsat|]. clear IHsz. - apply satisfies_var. - simpl. - unfold Valuation in *. - apply lookup_insert. - } - { - simpl in Hlf. inversion Hlf. - } - } - } - { - simpl in *. - apply satisfies_term_inv in Hsat. - destruct Hsat as [? [HContra ?]]. - inversion HContra. - } - } - { - simpl in *. - destruct φ. - { - simpl in *. - destruct a. - { - simpl in *. ltac1:(lia). - } - { - simpl in *. - rewrite filter_cons in Hlf. - destruct (decide (h = x)). - { - subst. simpl in *. - clear Hlf. - split>[apply Hsat|]. - apply satisfies_var. - unfold Valuation in *. - apply lookup_insert. - } - { - simpl in *. ltac1:(lia). - } - } - } - { - destruct (list_find (λ φi : TermOver BuiltinOrVar, h ∈ vars_of_to_l2r φi) l0) eqn:Hfind. - { - destruct p. - apply list_find_Some in Hfind. - destruct (l !! n) eqn:Hln. - { - apply satisfies_term_inv in Hsat. - destruct Hsat as [lγ [H1 [H2 H3]]]. - inversion H1; subst; clear H1. - simpl in *. - fold (@TermOverBoV_subst Σ) in *. - rewrite map_length in H2. - destruct Hfind as [Hfind1 [Hfind2 Hfind3]]. - specialize (IHsz t0 t). - ltac1:(ospecialize (IHsz _)). - { - apply take_drop_middle in Hln. - rewrite <- Hln in Hsz. simpl in Hsz. - rewrite sum_list_with_app in Hsz. simpl in Hsz. - ltac1:(lia). - } - specialize (IHsz Hnotinρ). - ltac1:(ospecialize (IHsz _)). - { - assert (Hlf' := Hlf). - apply take_drop_middle in Hfind1. - rewrite <- Hfind1 in Hlf. - rewrite map_app in Hlf. - rewrite map_cons in Hlf. - rewrite concat_app in Hlf. - rewrite concat_cons in Hlf. - rewrite filter_app in Hlf. - rewrite filter_app in Hlf. - rewrite list_filter_Forall_not in Hlf. - { - clear IHsz. simpl in Hlf. - rewrite app_length in Hlf. - ltac1:(rewrite -> list_filter_Forall_not with (l := (concat (map vars_of_to_l2r (drop (S n) l0)))) in Hlf). - { - simpl in Hlf. - rewrite Nat.add_0_r in Hlf. - exact Hlf. - } - { - apply not_Exists_Forall. - { intros ?. apply variable_eqdec. } - { - intros HContra. rewrite Exists_exists in HContra. - destruct HContra as [x [HContra ?]]. - subst x. - rewrite elem_of_list_lookup in HContra. - destruct HContra as [j1 HContra]. - apply take_drop_middle in HContra. - rewrite elem_of_list_lookup in Hfind2. - destruct Hfind2 as [j2 Hfind2]. - apply take_drop_middle in Hfind2. - rewrite <- Hfind2 in Hlf. - rewrite <- HContra in Hlf. - clear -Hlf. - rewrite filter_app in Hlf. - rewrite filter_app in Hlf. - rewrite filter_cons in Hlf. - rewrite filter_cons in Hlf. - destruct (decide (h=h))>[|ltac1:(contradiction)]. - simpl in Hlf. - rewrite app_length in Hlf. - rewrite app_length in Hlf. - simpl in Hlf. - ltac1:(lia). - } - } - } - { - clear -Hfind3. - rewrite Forall_forall. - intros x Hx. - rewrite elem_of_list_In in Hx. - rewrite in_concat in Hx. - destruct Hx as [x0 [H1x0 H2x0]]. - rewrite in_map_iff in H1x0. - destruct H1x0 as [x1 [H1x1 H2x1]]. - rewrite <- elem_of_list_In in H2x1. - rewrite <- elem_of_list_In in H2x0. - subst. intros HContra. subst. - rewrite elem_of_take in H2x1. - destruct H2x1 as [i [H1i H2i]]. - ltac1:(naive_solver). - } - } - specialize (IHsz Hnotinψ). - ltac1:(ospecialize (IHsz _)). - { - clear IHsz. - apply take_drop_middle in Hfind1. - apply take_drop_middle in Hln. - rewrite <- Hfind1 in H3. - rewrite <- Hln in H3. - rewrite map_app in H3. - rewrite map_cons in H3. - rewrite zip_with_app in H3. - { - rewrite Forall_app in H3. - simpl in H3. - rewrite Forall_cons in H3. - destruct H3 as [H31 [H32 H33]]. - exact H32. - } - { - rewrite take_length. - rewrite map_length. - rewrite take_length. - ltac1:(lia). - } - } - destruct IHsz as [IH1 IH2]. - split>[apply IH1|]. - unfold satisfies; simpl. - unfold apply_symbol'. - unfold to_PreTerm''. - unfold to_Term'. - constructor. - apply satisfies_top_bov_cons. - (repeat split); try reflexivity. - { - rewrite insert_length. ltac1:(lia). - } - { - assert (Hln' := Hln). - assert (Hfind1' := Hfind1). - apply take_drop_middle in Hln. - apply take_drop_middle in Hfind1. - rewrite <- Hln. - rewrite <- Hfind1. - rewrite insert_app_r_alt. - { - rewrite take_length. - rewrite Nat.min_l. - { - rewrite Nat.sub_diag. - simpl. - rewrite zip_with_app. - { - simpl. - rewrite Forall_app. - rewrite Forall_cons. - repeat split. - { - rewrite Forall_forall. - intros x Hx. - rewrite elem_of_lookup_zip_with in Hx. - destruct Hx as [i [x0 [y0 [HH1 [HH2 HH3]]]]]. - assert (Hi_lt_n : i < n). - { - apply lookup_lt_Some in HH2. - rewrite take_length in HH2. - ltac1:(lia). - } - subst x. - rewrite Forall_forall in H3. - ltac1:(setoid_rewrite elem_of_lookup_zip_with in H3). - eapply satisfies_ext>[|apply H3;exists i,x0,y0;(split>[reflexivity|])]. - { - unfold Valuation in *. - apply insert_subseteq. - clear -Hnotinρ. - unfold vars_of in Hnotinρ; simpl in Hnotinρ. - apply not_elem_of_dom_1. exact Hnotinρ. - } - { - rewrite lookup_take in HH2. - split>[exact HH2|]. - ltac1:(replace map with (@fmap _ list_fmap) by reflexivity). - rewrite list_lookup_fmap. - rewrite lookup_take in HH3. - rewrite HH3. - simpl. - rewrite subst_notin. - { reflexivity. } - { - intros HContra. - rewrite elem_of_list_lookup in HContra. - destruct HContra as [j Hj]. - apply take_drop_middle in Hj. - apply take_drop_middle in HH3. - rewrite <- HH3 in Hlf. - - rewrite map_app in Hlf. - rewrite map_cons in Hlf. - rewrite concat_app in Hlf. - rewrite concat_cons in Hlf. - rewrite filter_app in Hlf. - rewrite filter_app in Hlf. - rewrite <- Hj in Hlf. - clear Hj. - rewrite filter_app in Hlf. - rewrite filter_cons in Hlf. - destruct (decide (h=h))>[|ltac1:(contradiction)]. - clear e. - rewrite app_length in Hlf. - rewrite app_length in Hlf. - rewrite app_length in Hlf. - simpl in Hlf. - rewrite <- Hfind1 in Hlf. - assert (Hnl0: n < length l0). - { - apply lookup_lt_Some in Hfind1'. - exact Hfind1'. - } - (* clear -Hlf Hfind2 Hnl0. *) - apply elem_of_list_lookup in Hfind2. - destruct Hfind2 as [j' Hj']. - apply take_drop_middle in Hj'. - rewrite take_app in Hlf. - rewrite drop_app in Hlf. - rewrite take_length in Hlf. - destruct ((i - n `min` length l0)) eqn:Heq1. - { - simpl in Hlf. - destruct ((S i - n `min` length l0)) eqn:Heq2. - { - simpl in Hlf. - rewrite map_app in Hlf. - rewrite map_app in Hlf. - rewrite map_cons in Hlf. - simpl in Hlf. - rewrite concat_app in Hlf. - rewrite concat_app in Hlf. - rewrite concat_cons in Hlf. - rewrite <- Hj' in Hlf. - rewrite filter_app in Hlf. - rewrite filter_app in Hlf. - rewrite filter_app in Hlf. - rewrite filter_app in Hlf. - rewrite filter_cons in Hlf. - destruct (decide (h=h))>[|ltac1:(contradiction)]. - repeat (rewrite app_length in Hlf). - simpl in Hlf. - ltac1:(lia). - } - { - ltac1:(lia). - } - } - { - repeat (rewrite map_app in Hlf). - repeat (rewrite concat_app in Hlf). - repeat (rewrite filter_app in Hlf). - simpl in Hlf. - rewrite filter_app in Hlf. - rewrite <- Hj' in Hlf. - rewrite filter_app in Hlf. - rewrite filter_cons in Hlf. - destruct (decide (h=h))>[|ltac1:(contradiction)]. - repeat (rewrite app_length in Hlf). - simpl in Hlf. - ltac1:(lia). - } - } - { - ltac1:(lia). - } - { - ltac1:(lia). - } - } - } - { - exact IH2. - } - { - rewrite Forall_forall. - intros x Hx. - rewrite elem_of_lookup_zip_with in Hx. - destruct Hx as [i [x0 [y0 [HH1 [HH2 HH3]]]]]. - rewrite lookup_drop in HH2. - rewrite lookup_drop in HH3. - assert (S n + i < length l0). - { - apply lookup_lt_Some in HH3. - ltac1:(lia). - } - subst x. - rewrite Forall_forall in H3. - ltac1:(setoid_rewrite elem_of_lookup_zip_with in H3). - eapply satisfies_ext>[|apply H3;exists (S n + i),x0,y0;(split>[reflexivity|])]. - { - unfold Valuation in *. - apply insert_subseteq. - clear -Hnotinρ. - unfold vars_of in Hnotinρ; simpl in Hnotinρ. - apply not_elem_of_dom_1. exact Hnotinρ. - } - { - split>[exact HH2|]. - ltac1:(replace map with (@fmap _ list_fmap) by reflexivity). - rewrite list_lookup_fmap. - rewrite HH3. - simpl. - rewrite subst_notin. - { reflexivity. } - { - intros HContra. - rewrite elem_of_list_lookup in HContra. - destruct HContra as [j Hj]. - apply take_drop_middle in Hj. - apply take_drop_middle in HH3. - rewrite <- HH3 in Hlf. - - rewrite map_app in Hlf. - rewrite map_cons in Hlf. - rewrite concat_app in Hlf. - rewrite concat_cons in Hlf. - rewrite filter_app in Hlf. - rewrite filter_app in Hlf. - rewrite <- Hj in Hlf. - clear Hj. - rewrite filter_app in Hlf. - rewrite filter_cons in Hlf. - destruct (decide (h=h))>[|ltac1:(contradiction)]. - clear e. - rewrite app_length in Hlf. - rewrite app_length in Hlf. - rewrite app_length in Hlf. - simpl in Hlf. - rewrite <- Hfind1 in Hlf. - assert (Hnl0: n < length l0). - { - apply lookup_lt_Some in Hfind1'. - exact Hfind1'. - } - (* clear -Hlf Hfind2 Hnl0. *) - apply elem_of_list_lookup in Hfind2. - destruct Hfind2 as [j' Hj']. - apply take_drop_middle in Hj'. - rewrite take_app in Hlf. - rewrite drop_app in Hlf. - rewrite take_length in Hlf. - destruct (((S (n + i)) - n `min` length l0)) eqn:Heq1. - { - simpl in Hlf. - destruct ((S (S (n + i)) - n `min` length l0)) eqn:Heq2. - { - simpl in Hlf. - rewrite map_app in Hlf. - rewrite map_app in Hlf. - rewrite map_cons in Hlf. - simpl in Hlf. - rewrite concat_app in Hlf. - rewrite concat_app in Hlf. - rewrite concat_cons in Hlf. - rewrite <- Hj' in Hlf. - rewrite filter_app in Hlf. - rewrite filter_app in Hlf. - rewrite filter_app in Hlf. - rewrite filter_app in Hlf. - rewrite filter_cons in Hlf. - destruct (decide (h=h))>[|ltac1:(contradiction)]. - repeat (rewrite app_length in Hlf). - simpl in Hlf. - ltac1:(lia). - } - { - ltac1:(lia). - } - } - { - repeat (rewrite map_app in Hlf). - repeat (rewrite concat_app in Hlf). - repeat (rewrite filter_app in Hlf). - simpl in Hlf. - rewrite filter_app in Hlf. - rewrite <- Hj' in Hlf. - rewrite filter_app in Hlf. - rewrite filter_cons in Hlf. - destruct (decide (h=h))>[|ltac1:(contradiction)]. - repeat (rewrite app_length in Hlf). - simpl in Hlf. - ltac1:(lia). - } - } - } - } - } - { - rewrite take_length. - rewrite take_length. - ltac1:(lia). - } - } - { - apply lookup_lt_Some in Hln'. - ltac1:(lia). - } - } - { - rewrite take_length. ltac1:(lia). - } - } - } - { - simpl in *. - apply satisfies_term_inv in Hsat. - destruct Hsat as [lγ [H1 [H2 H3]]]. - inversion H1; subst; clear H1. - simpl in *. - rewrite map_length in H2. - destruct Hfind as [HContra ?]. - apply lookup_lt_Some in HContra. - apply lookup_ge_None in Hln. - ltac1:(lia). - } - } - { - apply list_find_None in Hfind. - simpl in *. - apply satisfies_term_inv in Hsat. - destruct Hsat as [lγ [H1 [H2 H3]]]. - inversion H1; subst; clear H1. - rewrite map_length in H2. - clear Heqmb. - ltac1:(exfalso). - clear -Hlf Hfind. - rewrite list_filter_Forall_not in Hlf. - { - simpl in Hlf. inversion Hlf. - } - { - clear -Hfind. - rewrite Forall_forall. - rewrite Forall_forall in Hfind. - intros x Hx. - rewrite elem_of_list_In in Hx. - rewrite in_concat in Hx. - destruct Hx as [x0 [H1x0 H2x0]]. - rewrite in_map_iff in H1x0. - destruct H1x0 as [x1 [H1x2 H2x1]]. - subst x0. - specialize (Hfind x1). - rewrite <- elem_of_list_In in H2x1. - specialize (Hfind H2x1). - intros HContra. subst x. - apply Hfind. - rewrite <- elem_of_list_In in H2x0. - apply H2x0. - } - } - } - } - } - } -Qed. -*) - - - -Lemma frto_step_app - {Σ : StaticModel} - (Act : Set) - : - forall - Γ - (t1 t2 t3 : TermOver builtin_value) - (w : list Act) - (a : Act) - r, - r ∈ Γ -> - flattened_rewrites_to_over Γ t1 w t2 -> - flattened_rewrites_to r (uglify' t2) a (uglify' t3) -> - flattened_rewrites_to_over Γ t1 (w++[a]) t3 -. -Proof. - intros Γ t1 t2 t3 w a r Hr H1 H2. - induction H1. - { - simpl. - eapply frto_step. - { exact Hr. } - { exact H2. } - { apply frto_base. } - } - { - simpl. - specialize (IHflattened_rewrites_to_over H2). - eapply frto_step. - { exact e. } - { exact f. } - { apply IHflattened_rewrites_to_over. } - } -Qed. - - -Lemma frto_app - {Σ : StaticModel} - (Act : Set) - : - forall - Γ - (t1 t2 t3 : TermOver builtin_value) - (w1 w2 : list Act), - flattened_rewrites_to_over Γ t1 w1 t2 -> - flattened_rewrites_to_over Γ t2 w2 t3 -> - flattened_rewrites_to_over Γ t1 (w1++w2) t3 -. -Proof. - intros. - revert t1 t2 t3 w2 X X0. - induction w1; intros t1 t2 t3 w2 H0 H1. - { - inversion H0; subst; clear H0. - simpl. - exact H1. - } - { - simpl. - inversion H0; subst; clear H0. - eapply frto_step>[|apply X|]. - { assumption. } - { - eapply IHw1. - { apply X0. } - { apply H1. } - } - } -Qed. - -Lemma satisfies_TermOver_vars_of - {Σ : StaticModel} - (ρ1 ρ2 : Valuation) - (g : TermOver builtin_value) - (φ : TermOver BuiltinOrVar) - : - (∀ x : variable, x ∈ vars_of (uglify' φ) → ρ1 !! x = ρ2 !! x) → - satisfies ρ1 g φ -> satisfies ρ2 g φ -. -Proof. - intros H. - assert (Htmp := satisfies_Term'_vars_of_1 ρ1 ρ2 (uglify' g) (uglify' φ) H). - apply Htmp. -Qed. - - -Lemma satisfies_PreTerm'Expression_vars_of - {Σ : StaticModel} - (ρ1 ρ2 : Valuation) - (g : PreTerm' symbol builtin_value) - (φ : PreTerm' symbol Expression) -: - (forall (x : variable), x ∈ vars_of φ -> ρ1!!x = ρ2!!x) -> - ( - satisfies ρ1 g φ - -> - satisfies ρ2 g φ - ) -. -Proof. - intros H1 H2. - apply matchesb_satisfies. - apply satisfies_matchesb in H2. - revert H1 H2. - revert φ. - induction g; intros φ Hvars; destruct φ; - unfold matchesb in *; unfold vars_of in *; - simpl in *; - try ltac1:(tauto). - { - do 2 (rewrite andb_true_iff). - intros [HH1 HH2]. - split. - { - apply IHg; try assumption. - ltac1:(set_solver). - } - unfold matchesb in *; simpl in *. - destruct - (decide (Expression_evaluate ρ1 b0 = Some (term_operand b))) as [Hsome1|Hnone1], - (decide (Expression_evaluate ρ2 b0 = Some (term_operand b))) as [Hsome2|Hnone2]. - { - rewrite Hsome1 in HH2. rewrite Hsome2. - exact HH2. - } - { - ltac1:(exfalso). - apply Hnone2. clear Hnone2. - assert (Hsome1' := Hsome1). - apply expression_evaluate_some_valuation in Hsome1'. - erewrite Expression_evaluate_val_restrict. - { apply Hsome1. } - unfold valuation_restrict. - rewrite map_filter_strong_ext. - intros i x. - simpl. - clear IHg. - specialize (Hvars i). - split; intros [HH'1 HH'2]; specialize (Hvars ltac:(set_solver)); - split; try assumption. - { - ltac1:(rewrite Hvars). assumption. - } - { - ltac1:(rewrite -Hvars). assumption. - } - } - { - ltac1:(exfalso). - apply Hnone1. clear Hnone1. - assert (Hsome2' := Hsome2). - apply expression_evaluate_some_valuation in Hsome2'. - erewrite Expression_evaluate_val_restrict. - { apply Hsome2. } - unfold valuation_restrict. - rewrite map_filter_strong_ext. - intros i x. - simpl. - clear IHg. - specialize (Hvars i). - split; intros [HH'1 HH'2]; specialize (Hvars ltac:(set_solver)); - split; try assumption. - { - ltac1:(rewrite -Hvars). assumption. - } - { - ltac1:(rewrite Hvars). assumption. - } - } - { - clear IHg Hvars. - rewrite bool_decide_eq_true in HH2. - rewrite bool_decide_eq_true. - ltac1:(tauto). - } - } - { - do 2 (rewrite andb_true_iff). - intros [HH1 HH2]. - split. - { - apply IHg. - ltac1:(set_solver). - assumption. - } - unfold matchesb in *; simpl in *. - ltac1:(tauto). - } - { - do 2 (rewrite andb_true_iff). - intros [HH1 HH2]. - split. - { - apply IHg1. - ltac1:(set_solver). - assumption. - } - unfold matchesb in *; simpl in *. - destruct - (decide (Expression_evaluate ρ1 b = Some (term_preterm g2))) as [Hsome1|Hnone1], - (decide (Expression_evaluate ρ2 b = Some (term_preterm g2))) as [Hsome2|Hnone2]. - { - rewrite Hsome1 in HH2. rewrite Hsome2. - assumption. - } - { - ltac1:(exfalso). - apply Hnone2. clear Hnone2. - assert (Hsome1' := Hsome1). - apply expression_evaluate_some_valuation in Hsome1'. - erewrite Expression_evaluate_val_restrict. - { apply Hsome1. } - unfold valuation_restrict. - rewrite map_filter_strong_ext. - intros i x. - simpl. - clear IHg. - specialize (Hvars i). - split; intros [HH'1 HH'2]; specialize (Hvars ltac:(set_solver)); - split; try assumption. - { - ltac1:(rewrite Hvars). assumption. - } - { - ltac1:(rewrite -Hvars). assumption. - } - } - { - ltac1:(exfalso). - apply Hnone1. clear Hnone1. - assert (Hsome2' := Hsome2). - apply expression_evaluate_some_valuation in Hsome2'. - erewrite Expression_evaluate_val_restrict. - { apply Hsome2. } - unfold valuation_restrict. - rewrite map_filter_strong_ext. - intros i x. - simpl. - clear IHg. - specialize (Hvars i). - split; intros [HH'1 HH'2]; specialize (Hvars ltac:(set_solver)); - split; try assumption. - { - ltac1:(rewrite -Hvars). assumption. - } - { - ltac1:(rewrite Hvars). assumption. - } - } - { - clear IHg Hvars. - rewrite bool_decide_eq_true in HH2. - rewrite bool_decide_eq_true. - ltac1:(tauto). - } - } - { - do 2 (rewrite andb_true_iff). - intros [HH1 HH2]. - split; ltac1:(set_solver). - } -Qed. - -Lemma satisfies_Term'Expression_vars_of - {Σ : StaticModel} - (ρ1 ρ2 : Valuation) - (g : Term' symbol builtin_value) - (φ : Term' symbol Expression) -: - (forall (x : variable), x ∈ vars_of φ -> ρ1!!x = ρ2!!x) -> - ( - satisfies ρ1 g φ - -> - satisfies ρ2 g φ - ) -. -Proof. - intros Hvars H1. - apply matchesb_satisfies. - apply satisfies_matchesb in H1. - revert H1. - destruct g, φ; unfold matchesb; simpl. - { - intros H1. - apply matchesb_satisfies in H1. - apply satisfies_matchesb. - eapply satisfies_PreTerm'Expression_vars_of. - apply Hvars. - apply H1. - } - { - unfold matchesb; simpl. - - destruct - (decide (Expression_evaluate ρ1 operand = Some (term_preterm ao))) as [Hsome1|Hnone1], - (decide (Expression_evaluate ρ2 operand = Some (term_preterm ao))) as [Hsome2|Hnone2]. - { - rewrite Hsome1. rewrite Hsome2. - ltac1:(tauto). - } - { - ltac1:(exfalso). - apply Hnone2. clear Hnone2. - assert (Hsome1' := Hsome1). - apply expression_evaluate_some_valuation in Hsome1'. - erewrite Expression_evaluate_val_restrict. - { apply Hsome1. } - unfold valuation_restrict. - rewrite map_filter_strong_ext. - intros i x. - simpl. - clear IHg. - specialize (Hvars i). - split; intros [HH1 HH2]; specialize (Hvars ltac:(set_solver)); - split; try assumption. - { - ltac1:(rewrite Hvars). assumption. - } - { - ltac1:(rewrite -Hvars). assumption. - } - } - { - ltac1:(exfalso). - apply Hnone1. clear Hnone1. - assert (Hsome2' := Hsome2). - apply expression_evaluate_some_valuation in Hsome2'. - erewrite Expression_evaluate_val_restrict. - { apply Hsome2. } - unfold valuation_restrict. - rewrite map_filter_strong_ext. - intros i x. - simpl. - clear IHg. - specialize (Hvars i). - split; intros [HH1 HH2]; specialize (Hvars ltac:(set_solver)); - split; try assumption. - { - ltac1:(rewrite -Hvars). assumption. - } - { - ltac1:(rewrite Hvars). assumption. - } - } - { - clear IHg Hvars. - rewrite bool_decide_eq_true. - rewrite bool_decide_eq_true. - ltac1:(tauto). - } - } - { - ltac1:(tauto). - } - { - unfold matchesb; simpl. - - - destruct - (decide (Expression_evaluate ρ1 operand0 = Some (term_operand operand))) as [Hsome1|Hnone1], - (decide (Expression_evaluate ρ2 operand0 = Some (term_operand operand))) as [Hsome2|Hnone2]. - { - rewrite Hsome1. rewrite Hsome2. - ltac1:(tauto). - } - { - ltac1:(exfalso). - apply Hnone2. clear Hnone2. - assert (Hsome1' := Hsome1). - apply expression_evaluate_some_valuation in Hsome1'. - erewrite Expression_evaluate_val_restrict. - { apply Hsome1. } - unfold valuation_restrict. - rewrite map_filter_strong_ext. - intros i x. - simpl. - clear IHg. - specialize (Hvars i). - split; intros [HH1 HH2]; specialize (Hvars ltac:(set_solver)); - split; try assumption. - { - ltac1:(rewrite Hvars). assumption. - } - { - ltac1:(rewrite -Hvars). assumption. - } - } - { - ltac1:(exfalso). - apply Hnone1. clear Hnone1. - assert (Hsome2' := Hsome2). - apply expression_evaluate_some_valuation in Hsome2'. - erewrite Expression_evaluate_val_restrict. - { apply Hsome2. } - unfold valuation_restrict. - rewrite map_filter_strong_ext. - intros i x. - simpl. - clear IHg. - specialize (Hvars i). - split; intros [HH1 HH2]; specialize (Hvars ltac:(set_solver)); - split; try assumption. - { - ltac1:(rewrite -Hvars). assumption. - } - { - ltac1:(rewrite Hvars). assumption. - } - } - { - clear IHg Hvars. - rewrite bool_decide_eq_true. - rewrite bool_decide_eq_true. - ltac1:(tauto). - } - } -Qed. - -Lemma satisfies_TermOverExpression_vars_of - {Σ : StaticModel} - (ρ1 ρ2 : Valuation) - (g : TermOver builtin_value) - (φ : TermOver Expression) - : - (∀ x : variable, x ∈ vars_of (uglify' φ) → ρ1 !! x = ρ2 !! x) → - satisfies ρ1 g φ -> satisfies ρ2 g φ -. -Proof. - intros H. - assert (Htmp := satisfies_Term'Expression_vars_of ρ1 ρ2 (uglify' g) (uglify' φ) H). - apply Htmp. -Qed. - -Lemma valaution_restrict_subseteq - {Σ : StaticModel} - (e : Expression) - (ρ1 ρ2 : Valuation) - : - (∀ x : variable, x ∈ vars_of e → ρ1 !! x = ρ2 !! x) -> - vars_of e ⊆ vars_of ρ1 -> - vars_of e ⊆ vars_of ρ2 -> - valuation_restrict ρ1 (vars_of e) = valuation_restrict ρ2 (vars_of e) -. -Proof. - intros HH H1 H2. - unfold valuation_restrict. - rewrite map_filter_strong_ext. - intros i x. simpl. - rewrite elem_of_subseteq in H1. - rewrite elem_of_subseteq in H2. - specialize (H1 i). - specialize (H2 i). - unfold vars_of in H1; simpl in H1. - unfold vars_of in H2; simpl in H2. - rewrite elem_of_dom in H1. - rewrite elem_of_dom in H2. - split; intros [H3 H4]; specialize (H1 H3); specialize (H2 H3); - split; try assumption. - { - destruct H1 as [x1 Hx1]. - destruct H2 as [x2 Hx2]. - specialize (HH i H3). - ltac1:(rewrite HH in H4). - exact H4. - } - { - destruct H1 as [x1 Hx1]. - destruct H2 as [x2 Hx2]. - specialize (HH i H3). - ltac1:(rewrite HH). - exact H4. - } -Qed. - -Lemma val_elem_of_dom_1 - {Σ : StaticModel} - (ρ : gmap variable GroundTerm) - (x : variable) - : - x ∈ dom ρ -> isSome (ρ !! x) = true -. -Proof. - rewrite elem_of_dom. - destruct (ρ!!x); simpl. - { - intros _. reflexivity. - } - { - intros H. unfold is_Some in H. - destruct H as [x0 Hx0]. - inversion Hx0. - } -Qed. - -Lemma satisfies_scs_vars_of - {Σ : StaticModel} - (ρ1 ρ2 : Valuation) - (scs : list SideCondition) - : - (∀ x : variable, x ∈ vars_of scs → ρ1 !! x = ρ2 !! x) → - satisfies ρ1 () scs -> satisfies ρ2 () scs -. -Proof. - intros H. - unfold satisfies; simpl. - induction scs. - { - intros HH1 HH2 HH3. - rewrite elem_of_nil in HH3. - inversion HH3. - } - { - intros HH x Hx. - - destruct (decide (x = a)). - { - specialize (HH x Hx). - rewrite elem_of_cons in Hx. - subst x. - clear -HH H. - unfold satisfies in *; simpl in *. - unfold valuation_satisfies_sc in *; simpl in *. - destruct a as [c]. - unfold satisfies in *; simpl in *. - unfold val_satisfies_ap in *; simpl in *. - destruct c as [e1 e2]. - - destruct HH as [HH1 HH2]. - unfold isSome in *. - (destruct (Expression_evaluate ρ1 e1) as [x11|] eqn:H11)>[|inversion HH2]. - symmetry in HH1. clear HH2. - apply expression_evaluate_some_valuation in HH1 as Hx11'. - apply expression_evaluate_some_valuation in H11 as Hx12'. - - assert (H2: vars_of e1 ⊆ vars_of ρ2). - { - rewrite elem_of_subseteq in Hx11'. - rewrite elem_of_subseteq. - intros x Hx. - specialize (H x). - unfold vars_of in H; simpl in H. - unfold vars_of at 1 in H; simpl in H. - unfold vars_of at 1 in H; simpl in H. - specialize (H ltac:(set_solver)). - unfold vars_of; simpl. - - rewrite elem_of_subseteq in Hx12'. - specialize (Hx12' x Hx). - unfold vars_of in Hx12'; simpl in Hx12'. - apply val_elem_of_dom_1 in Hx12'. - unfold Valuation in *. - unfold isSome in *. - destruct (ρ1 !! x)>[|inversion Hx12']. - eapply elem_of_dom_2. - rewrite <- H. - reflexivity. - } - assert (H3: vars_of e2 ⊆ vars_of ρ2). - { - rewrite elem_of_subseteq in Hx11'. - rewrite elem_of_subseteq. - intros x Hx. - specialize (H x). - unfold vars_of in H; simpl in H. - unfold vars_of at 1 in H; simpl in H. - unfold vars_of at 1 in H; simpl in H. - specialize (H ltac:(set_solver)). - unfold vars_of; simpl. - unfold Valuation in *. - - specialize (Hx11' x Hx). - unfold vars_of in Hx11'; simpl in Hx11'. - apply val_elem_of_dom_1 in Hx11'. - unfold isSome in Hx11'. - destruct (ρ1 !! x) eqn:Htmp>[|inversion Hx11']. - eapply elem_of_dom_2. - rewrite <- H. - reflexivity. - } - - apply Expression_evalute_total_T_2 in H2 as H2'. - apply Expression_evalute_total_T_2 in H3 as H3'. - destruct H2' as [g2 H2']. - destruct H3' as [g3 H3']. - rewrite H2'. rewrite <- H2'. - split>[|reflexivity]. - assert (Some g2 = Some x11). - { - rewrite <- H11. - rewrite <- H2'. - apply Expression_evaluate_val_restrict. - unfold valuation_restrict. - rewrite map_filter_strong_ext. - intros i x. simpl. - split; intros [HH'1 HH'2]. - { - rewrite H. - { - unfold Valuation in *. - rewrite HH'2. - split>[assumption|reflexivity]. - } - { - unfold vars_of; simpl. - unfold vars_of at 1; simpl. - unfold vars_of at 1; simpl. - ltac1:(set_solver). - } - } - { - rewrite <- H. - { - unfold Valuation in *. - rewrite HH'2. - split>[assumption|reflexivity]. - } - { - unfold vars_of; simpl. - unfold vars_of at 1; simpl. - unfold vars_of at 1; simpl. - ltac1:(set_solver). - } - } - } - assert (Some g3 = Some x11). - { - rewrite <- HH1. - rewrite <- H3'. - apply Expression_evaluate_val_restrict. - unfold valuation_restrict. - rewrite map_filter_strong_ext. - intros i x. simpl. - split; intros [HH'1 HH'2]. - { - rewrite H. - { - unfold Valuation in *. - rewrite HH'2. - split>[assumption|reflexivity]. - } - { - unfold vars_of; simpl. - unfold vars_of at 1; simpl. - unfold vars_of at 1; simpl. - ltac1:(set_solver). - } - } - { - rewrite <- H. - { - unfold Valuation in *. - rewrite HH'2. - split>[assumption|reflexivity]. - } - { - unfold vars_of; simpl. - unfold vars_of at 1; simpl. - unfold vars_of at 1; simpl. - ltac1:(set_solver). - } - } - } - ltac1:(congruence). - } - { - assert (x ∈ scs) by ltac1:(set_solver). - specialize (IHscs ltac:(set_solver)). - eapply IHscs>[|assumption]. - intros x0 Hx0. - exact (HH x0 ltac:(set_solver)). - } - } -Qed. - -Lemma satisfies_TermOverBoV_to_TermOverExpr - {Σ : StaticModel} - (ρ : Valuation) - (γ : TermOver builtin_value) - (φ : TermOver BuiltinOrVar) - : - satisfies ρ γ (TermOverBoV_to_TermOverExpr φ) - -> - satisfies ρ γ φ -. -Proof. - revert γ. - ltac1:(induction φ using TermOver_rect); intros γ. - { - unfold TermOverBoV_to_TermOverExpr. - simpl. - intros H. - { - destruct a; simpl in *. - { - inversion H; subst; clear H. - { - apply (f_equal prettify) in H2. - rewrite (cancel prettify uglify') in H2. - subst γ. - constructor. - inversion pf; subst; clear pf. - constructor. - } - { - apply (f_equal prettify) in H2. - rewrite (cancel prettify uglify') in H2. - subst γ. - inversion X. - } - } - { - inversion H; subst; clear H. - { - apply (f_equal prettify) in H2. - rewrite (cancel prettify uglify') in H2. - subst γ. - constructor. - inversion pf; subst; clear pf. - constructor. - assumption. - } - { - apply (f_equal prettify) in H2. - rewrite (cancel prettify uglify') in H2. - subst γ. - inversion X; subst; clear X. - simpl. - apply satisfies_var. - rewrite uglify'_prettify'. + apply (f_equal prettify) in H2. + rewrite (cancel prettify uglify') in H2. + subst γ. + inversion X; subst; clear X. + simpl. + apply satisfies_var. + rewrite uglify'_prettify'. assumption. } } @@ -8089,770 +6701,7 @@ Proof. } Qed. - -Lemma factor_by_subst_correct_2 - {Σ : StaticModel} - (sz : nat) - (ρ : Valuation) - (h : variable) - (γ : TermOver builtin_value) - (φ ψ : TermOver BuiltinOrVar) - : sz >= TermOver_size γ -> - length (filter (eq h) (vars_of_to_l2r φ)) = 1 -> - ~ (h ∈ vars_of_to_l2r ψ) -> - satisfies ρ γ (TermOverBoV_subst φ h ψ) -> - let xy := factor_by_subst sz ρ h γ φ ψ in - ((satisfies ρ xy.2 ψ) * - (satisfies (<[h := (uglify' xy.2)]>ρ) xy.1 φ))%type -. -Proof. - revert γ φ. - induction sz; intros γ φ Hsz. - { - destruct γ; simpl in Hsz; ltac1:(lia). - } - { - intros Hlf Hnotinψ Hsat. - unfold factor_by_subst. fold (@factor_by_subst Σ). - simpl. - destruct (matchesb ρ (uglify' γ) (uglify' ψ)) eqn:Heqmb. - { - simpl. - split. - { - apply matchesb_satisfies in Heqmb. - unfold satisfies; simpl. - apply Heqmb. - } - { - apply matchesb_satisfies in Heqmb. - assert (Heqmb': satisfies ρ γ ψ). - { - unfold satisfies; simpl. - apply Heqmb. - } - - assert (Htmp2 := TermOver_size_not_zero ψ). - assert (Htmp3 := TermOver_size_not_zero φ). - assert (Hsat' := Hsat). - apply concrete_is_larger_than_symbolic in Hsat'. - apply concrete_is_larger_than_symbolic in Heqmb'. - - unfold delta_in_val in Hsat'. - assert (Hperm := vars_of_to_l2r_subst φ ψ h Hlf Hnotinψ). - apply sum_list_with_perm with (f := (size_of_var_in_val ρ)) in Hperm. - rewrite Hperm in Hsat'. clear Hperm. - rewrite TermOverBoV_subst_once_size in Hsat'. - { - - rewrite sum_list_with_app in Hsat'. - unfold delta_in_val in Heqmb'. - assert (Hszφ: TermOver_size φ = 1) by ltac1:(lia). - clear Hsat. - destruct φ. - { - simpl in *. clear Hszφ. - clear Htmp3. - destruct a. - { - simpl in *. ltac1:(lia). - } - simpl in *. rewrite filter_cons in Hlf. - destruct (decide (h = x)). - { - subst. - clear Heqmb' Hsat' Htmp2. clear Hlf. - simpl. - apply satisfies_var. - unfold Valuation in *. - apply lookup_insert. - } - { - simpl in *. ltac1:(lia). - } - } - { - simpl in Hszφ. - destruct l. - { - simpl in *. clear Hszφ Htmp3 Heqmb' Hsat'. - ltac1:(lia). - } - { - simpl in *. - ltac1:(lia). - } - } - } - { - rewrite <- vars_of_uglify. - assumption. - } - { - assumption. - } - } - } - { - destruct γ. - { - destruct φ. - { - destruct a0; simpl in *. - { - ltac1:(lia). - } - { - rewrite filter_cons in Hlf. - destruct (decide (h = x)). - { - subst. simpl in *. clear Hlf. - split>[exact Hsat|]. clear IHsz. - apply satisfies_var. - simpl. - unfold Valuation in *. - apply lookup_insert. - } - { - simpl in Hlf. inversion Hlf. - } - } - } - { - simpl in *. - apply satisfies_term_bov_inv in Hsat. - destruct Hsat as [HContra0 [[HContra10 HContra11] HContra2]]. - inversion HContra10. - } - } - { - simpl in *. - destruct φ. - { - simpl in *. - destruct a. - { - simpl in *. ltac1:(lia). - } - { - simpl in *. - rewrite filter_cons in Hlf. - destruct (decide (h = x)). - { - subst. simpl in *. - clear Hlf. - split>[apply Hsat|]. - apply satisfies_var. - unfold Valuation in *. - apply lookup_insert. - } - { - simpl in *. ltac1:(lia). - } - } - } - { - destruct (list_find (λ φi : TermOver BuiltinOrVar, h ∈ vars_of_to_l2r φi) l0) eqn:Hfind. - { - destruct p. - apply list_find_Some in Hfind. - destruct (l !! n) eqn:Hln. - { - apply satisfies_term_bov_inv in Hsat. - destruct Hsat as [lγ [[H1 H2] H3]]. - inversion H1; subst; clear H1. - simpl in *. - fold (@TermOverBoV_subst Σ) in *. - rewrite map_length in H2. - destruct Hfind as [Hfind1 [Hfind2 Hfind3]]. - specialize (IHsz t0 t). - ltac1:(ospecialize (IHsz _)). - { - apply take_drop_middle in Hln. - rewrite <- Hln in Hsz. simpl in Hsz. - rewrite sum_list_with_app in Hsz. simpl in Hsz. - ltac1:(lia). - } - - ltac1:(ospecialize (IHsz _)). - { - assert (Hlf' := Hlf). - apply take_drop_middle in Hfind1. - rewrite <- Hfind1 in Hlf. - rewrite map_app in Hlf. - rewrite map_cons in Hlf. - rewrite concat_app in Hlf. - rewrite concat_cons in Hlf. - rewrite filter_app in Hlf. - rewrite filter_app in Hlf. - rewrite list_filter_Forall_not in Hlf. - { - clear IHsz. simpl in Hlf. - rewrite app_length in Hlf. - ltac1:(rewrite -> list_filter_Forall_not with (l := (concat (map vars_of_to_l2r (drop (S n) l0)))) in Hlf). - { - simpl in Hlf. - rewrite Nat.add_0_r in Hlf. - exact Hlf. - } - { - apply not_Exists_Forall. - { intros ?. apply variable_eqdec. } - { - intros HContra. rewrite Exists_exists in HContra. - destruct HContra as [x [HContra ?]]. - subst x. - rewrite elem_of_list_lookup in HContra. - destruct HContra as [j1 HContra]. - apply take_drop_middle in HContra. - rewrite elem_of_list_lookup in Hfind2. - destruct Hfind2 as [j2 Hfind2]. - apply take_drop_middle in Hfind2. - rewrite <- Hfind2 in Hlf. - unfold TermOver in *. - rewrite <- HContra in Hlf. - clear -Hlf. - rewrite filter_app in Hlf. - rewrite filter_app in Hlf. - rewrite filter_cons in Hlf. - rewrite filter_cons in Hlf. - destruct (decide (h=h))>[|ltac1:(contradiction)]. - simpl in Hlf. - rewrite app_length in Hlf. - rewrite app_length in Hlf. - simpl in Hlf. - ltac1:(lia). - } - } - } - { - clear -Hfind3. - rewrite Forall_forall. - intros x Hx. - rewrite elem_of_list_In in Hx. - rewrite in_concat in Hx. - destruct Hx as [x0 [H1x0 H2x0]]. - rewrite in_map_iff in H1x0. - destruct H1x0 as [x1 [H1x1 H2x1]]. - rewrite <- elem_of_list_In in H2x1. - rewrite <- elem_of_list_In in H2x0. - subst. intros HContra. subst. - rewrite elem_of_take in H2x1. - destruct H2x1 as [i [H1i H2i]]. - ltac1:(naive_solver). - } - } - specialize (IHsz Hnotinψ). - ltac1:(ospecialize (IHsz _)). - { - clear IHsz. - apply take_drop_middle in Hfind1. - apply take_drop_middle in Hln. - rewrite <- Hfind1 in H3. - rewrite <- Hln in H3. - rewrite map_app in H3. - rewrite map_cons in H3. - eapply H3 with (i := length (take n lγ)). - { - rewrite lookup_app_r. - { - rewrite Nat.sub_diag. reflexivity. - } - { - ltac1:(lia). - } - } - { - rewrite lookup_app_r. - { - rewrite take_length. - rewrite map_length. - rewrite take_length. - rewrite H2. - rewrite Nat.sub_diag. - simpl. - reflexivity. - } - { - rewrite take_length. - rewrite map_length. - rewrite take_length. - ltac1:(lia). - } - } - } - destruct IHsz as [IH1 IH2]. - split>[apply IH1|]. - unfold satisfies; simpl. - unfold apply_symbol'. - unfold to_PreTerm''. - unfold to_Term'. - constructor. - apply satisfies_top_bov_cons_1. - { - rewrite insert_length. ltac1:(lia). - } - { reflexivity. } - { - assert (Hln' := Hln). - assert (Hfind1' := Hfind1). - apply take_drop_middle in Hln. - apply take_drop_middle in Hfind1. - rewrite <- Hln. - rewrite <- Hfind1. - rewrite insert_app_r_alt. - { - rewrite take_length. - rewrite Nat.min_l. - { - rewrite Nat.sub_diag. - simpl. - intros i s l. - intros H1i H2i. - destruct (decide (i < length (take n lγ))) as [Hlt|Hge]. - { - rewrite lookup_app_l in H1i>[|ltac1:(lia)]. - rewrite lookup_app_l in H2i. - { - eapply satisfies_TermOver_vars_of>[|eapply H3]. - { - intros x Hx. - destruct (decide (h = x)). - { - subst. - ltac1:(exfalso). - rewrite <- vars_of_uglify in Hx. - - rewrite elem_of_list_lookup in Hx. - destruct Hx as [j Hj]. - apply take_drop_middle in Hj. - rewrite lookup_take in H2i>[|(apply lookup_lt_Some in H2i;rewrite take_length in H2i; ltac1:(lia))]. - apply take_drop_middle in H2i. - rewrite <- H2i in Hlf. - rewrite map_app in Hlf. simpl in Hlf. - rewrite <- Hj in Hlf. - rewrite take_length in Hlt. - (* TODO simplify Hlf and then use Hfind1 *) - rewrite concat_app in Hlf. - simpl in Hlf. - rewrite filter_app in Hlf; simpl in Hlf. - rewrite filter_app in Hlf; simpl in Hlf. - rewrite filter_app in Hlf; simpl in Hlf. - rewrite filter_cons in Hlf. - destruct (decide (x=x))>[|ltac1:(congruence)]. - rewrite app_length in Hlf; simpl in Hlf. - rewrite app_length in Hlf; simpl in Hlf. - rewrite app_length in Hlf; simpl in Hlf. - rewrite <- Hfind1 in Hlf. - rewrite drop_app in Hlf. - unfold TermOver in *. - destruct (((S i - length (take n l0)))) eqn:Htmp1; simpl in *. - { - rewrite map_app in Hlf; simpl in Hlf. - rewrite concat_app in Hlf; simpl in Hlf. - rewrite filter_app in Hlf; simpl in Hlf. - rewrite elem_of_list_lookup in Hfind2. - destruct Hfind2 as [j3 Hj3]. - apply take_drop_middle in Hj3. - rewrite <- Hj3 in Hlf. - rewrite filter_app in Hlf; simpl in Hlf. - rewrite filter_app in Hlf; simpl in Hlf. - rewrite filter_cons in Hlf. - destruct (decide (x=x))>[|ltac1:(congruence)]. - repeat (rewrite app_length in Hlf). - simpl in Hlf. - ltac1:(lia). - } - { - rewrite take_length in Htmp1. - ltac1:(lia). - } - } - { - unfold Valuation in *. - rewrite lookup_insert_ne>[reflexivity|ltac1:(congruence)]. - } - } - { - rewrite lookup_take in H1i. - { - apply H1i. - } - { - apply lookup_lt_Some in H1i. - rewrite take_length in Hlt. - ltac1:(lia). - } - } - { - ltac1:(replace (map) with (@fmap _ list_fmap) by reflexivity). - rewrite list_lookup_fmap. - rewrite lookup_take in H2i. - { - rewrite H2i. - simpl. - rewrite subst_notin. - { reflexivity. } - { - intros HContra. - rewrite elem_of_list_lookup in HContra. - destruct HContra as [j Hj]. - apply take_drop_middle in Hj. - assert (HH3 := H2i). - apply take_drop_middle in HH3. - rewrite <- HH3 in Hlf. - - rewrite map_app in Hlf. - rewrite map_cons in Hlf. - rewrite concat_app in Hlf. - rewrite concat_cons in Hlf. - rewrite filter_app in Hlf. - rewrite filter_app in Hlf. - rewrite <- Hj in Hlf. - clear Hj. - rewrite filter_app in Hlf. - rewrite filter_cons in Hlf. - destruct (decide (h=h))>[|ltac1:(contradiction)]. - clear e. - rewrite app_length in Hlf. - rewrite app_length in Hlf. - rewrite app_length in Hlf. - simpl in Hlf. - rewrite <- Hfind1 in Hlf. - assert (Hnl0: n < length l0). - { - apply lookup_lt_Some in Hfind1'. - exact Hfind1'. - } - (* clear -Hlf Hfind2 Hnl0. *) - apply elem_of_list_lookup in Hfind2. - destruct Hfind2 as [j' Hj']. - apply take_drop_middle in Hj'. - rewrite take_app in Hlf. - rewrite drop_app in Hlf. - rewrite take_length in Hlf. - unfold TermOver in *. - destruct ((i - n `min` length l0)) eqn:Heq1. - { - simpl in Hlf. - destruct ((S i - n `min` length l0)) eqn:Heq2. - { - simpl in Hlf. - rewrite map_app in Hlf. - rewrite map_app in Hlf. - rewrite map_cons in Hlf. - simpl in Hlf. - rewrite concat_app in Hlf. - rewrite concat_app in Hlf. - rewrite concat_cons in Hlf. - rewrite <- Hj' in Hlf. - rewrite filter_app in Hlf. - rewrite filter_app in Hlf. - rewrite filter_app in Hlf. - rewrite filter_app in Hlf. - rewrite filter_cons in Hlf. - destruct (decide (h=h))>[|ltac1:(contradiction)]. - repeat (rewrite app_length in Hlf). - simpl in Hlf. - ltac1:(lia). - } - { - rewrite take_length in Hlt. - ltac1:(lia). - } - } - { - repeat (rewrite map_app in Hlf). - repeat (rewrite concat_app in Hlf). - repeat (rewrite filter_app in Hlf). - simpl in Hlf. - rewrite filter_app in Hlf. - rewrite <- Hj' in Hlf. - rewrite filter_app in Hlf. - rewrite filter_cons in Hlf. - destruct (decide (h=h))>[|ltac1:(contradiction)]. - repeat (rewrite app_length in Hlf). - simpl in Hlf. - ltac1:(lia). - } - } - } - { - apply lookup_lt_Some in H2i. - rewrite take_length in Hlt. - ltac1:(lia). - } - } - } - { - rewrite take_length. - rewrite take_length in Hlt. - ltac1:(lia). - } - } - - destruct (decide (((length (take n lγ))) < i)) as [Hlt'|Hge']. - { - rewrite lookup_app_r in H1i>[|ltac1:(lia)]. - destruct ((i - length (take n lγ))) eqn:Htmp1>[ltac1:(lia)|]. - rewrite lookup_app_r in H2i. - { - unfold TermOver in *. - destruct ((i - length (take n l0))) eqn:Htmp2> - [ - rewrite take_length in Hlt'; - rewrite take_length in Htmp2; - rewrite take_length in Htmp1; - rewrite take_length in Hge; - ltac1:(lia) - |]. - eapply satisfies_TermOver_vars_of>[|eapply H3]. - { - intros x Hx. - destruct (decide (h = x)). - { - subst. - ltac1:(exfalso). - rewrite <- vars_of_uglify in Hx. - - rewrite elem_of_list_lookup in Hx. - destruct Hx as [j Hj]. - apply take_drop_middle in Hj. - simpl in H2i. - rewrite lookup_drop in H2i. - apply take_drop_middle in H2i. - rewrite <- H2i in Hlf. - rewrite map_app in Hlf. simpl in Hlf. - rewrite <- Hj in Hlf. - (*rewrite take_length in Hlt.*) - (* TODO simplify Hlf and then use Hfind1 *) - rewrite concat_app in Hlf. - simpl in Hlf. - rewrite filter_app in Hlf; simpl in Hlf. - rewrite filter_app in Hlf; simpl in Hlf. - rewrite filter_app in Hlf; simpl in Hlf. - rewrite filter_cons in Hlf. - destruct (decide (x=x))>[|ltac1:(congruence)]. - rewrite app_length in Hlf; simpl in Hlf. - rewrite app_length in Hlf; simpl in Hlf. - rewrite app_length in Hlf; simpl in Hlf. - rewrite <- Hfind1 in Hlf. - rewrite drop_app in Hlf. - rewrite take_app in Hlf. - destruct ((S (n + n1) - length (take n l0))) eqn:Htmp3; simpl in *. - { - rewrite take_length in Htmp3. - ltac1:(lia). - } - { - rewrite map_app in Hlf; simpl in Hlf. - rewrite concat_app in Hlf; simpl in Hlf. - rewrite filter_app in Hlf; simpl in Hlf. - rewrite elem_of_list_lookup in Hfind2. - destruct Hfind2 as [j3 Hj3]. - apply take_drop_middle in Hj3. - rewrite <- Hj3 in Hlf. - rewrite filter_app in Hlf; simpl in Hlf. - rewrite filter_app in Hlf; simpl in Hlf. - rewrite filter_cons in Hlf. - destruct (decide (x=x))>[|ltac1:(congruence)]. - repeat (rewrite app_length in Hlf). - simpl in Hlf. - ltac1:(lia). - } - } - { - unfold Valuation in *. - rewrite lookup_insert_ne>[reflexivity|ltac1:(congruence)]. - } - } - { - simpl in H1i. - rewrite lookup_drop in H1i. - apply H1i. - } - { - ltac1:(replace (map) with (@fmap _ list_fmap) by reflexivity). - rewrite list_lookup_fmap. - simpl in H2i. - rewrite lookup_drop in H2i. - assert (n0 = n1). - { - rewrite take_length in Htmp1. - rewrite take_length in Htmp2. - ltac1:(lia). - } - subst n1. - rewrite H2i. - simpl. - rewrite subst_notin. - { reflexivity. } - { - intros HContra. - rewrite elem_of_list_lookup in HContra. - destruct HContra as [j Hj]. - apply take_drop_middle in Hj. - assert (HH3 := H2i). - apply take_drop_middle in HH3. - rewrite <- HH3 in Hlf. - - rewrite map_app in Hlf. - rewrite map_cons in Hlf. - rewrite concat_app in Hlf. - rewrite concat_cons in Hlf. - rewrite filter_app in Hlf. - rewrite filter_app in Hlf. - rewrite <- Hj in Hlf. - clear Hj. - rewrite filter_app in Hlf. - rewrite filter_cons in Hlf. - destruct (decide (h=h))>[|ltac1:(contradiction)]. - clear e. - rewrite app_length in Hlf. - rewrite app_length in Hlf. - rewrite app_length in Hlf. - simpl in Hlf. - rewrite <- Hfind1 in Hlf. - assert (Hnl0: n < length l0). - { - apply lookup_lt_Some in Hfind1'. - exact Hfind1'. - } - (* clear -Hlf Hfind2 Hnl0. *) - apply elem_of_list_lookup in Hfind2. - destruct Hfind2 as [j' Hj']. - apply take_drop_middle in Hj'. - rewrite take_app in Hlf. - rewrite drop_app in Hlf. - rewrite take_length in Hlf. - - destruct ((S (n + n0) - n `min` length l0)) eqn:Heq1. - { - simpl in Hlf. - ltac1:(lia). - } - { - simpl in Hlf. - rewrite map_app in Hlf. - rewrite map_app in Hlf. - rewrite map_cons in Hlf. - simpl in Hlf. - rewrite concat_app in Hlf. - rewrite concat_app in Hlf. - rewrite concat_cons in Hlf. - rewrite <- Hj' in Hlf. - rewrite filter_app in Hlf. - rewrite filter_app in Hlf. - rewrite filter_app in Hlf. - rewrite filter_app in Hlf. - rewrite filter_cons in Hlf. - destruct (decide (h=h))>[|ltac1:(contradiction)]. - repeat (rewrite app_length in Hlf). - simpl in Hlf. - ltac1:(lia). - } - } - } - } - { - rewrite take_length. - rewrite take_length in Hlt'. - ltac1:(lia). - } - } - assert (i = length (take n lγ)). - { - ltac1:(lia). - } - subst i. - rewrite lookup_app_r in H2i. - rewrite lookup_app_r in H1i. - rewrite take_length in H2i. - rewrite take_length in H2i. - rewrite Nat.sub_diag in H1i. - simpl in H1i. - rewrite H2 in H2i. - rewrite Nat.sub_diag in H2i. - simpl in H2i. - inversion H2i; subst; clear H2i. - inversion H1i; subst; clear H1i. - exact IH2. - { - repeat (rewrite take_length). - ltac1:(lia). - } - { - repeat (rewrite take_length). - ltac1:(lia). - } - } - { - apply lookup_lt_Some in Hln'. - ltac1:(lia). - } - } - { - rewrite take_length. ltac1:(lia). - } - } - } - { - simpl in *. - destruct Hfind as [Hfind1 [Hfind2 Hfind3]]. - apply lookup_lt_Some in Hfind1. - apply lookup_ge_None in Hln. - - - apply satisfies_term_bov_inv in Hsat. - destruct Hsat as [lγ [[H1 H2] H3]]. - inversion H1; subst; clear H1. - simpl in *. - rewrite map_length in H2. - ltac1:(lia). - } - } - { - simpl in *. - apply list_find_None in Hfind. - simpl in *. - apply satisfies_term_bov_inv in Hsat. - destruct Hsat as [lγ [[H1 H2] H3]]. - inversion H1; subst; clear H1. - rewrite map_length in H2. - clear Heqmb. - ltac1:(exfalso). - clear -Hlf Hfind. - rewrite list_filter_Forall_not in Hlf. - { - simpl in Hlf. inversion Hlf. - } - { - clear -Hfind. - rewrite Forall_forall. - rewrite Forall_forall in Hfind. - intros x Hx. - rewrite elem_of_list_In in Hx. - rewrite in_concat in Hx. - destruct Hx as [x0 [H1x0 H2x0]]. - rewrite in_map_iff in H1x0. - destruct H1x0 as [x1 [H1x2 H2x1]]. - subst x0. - specialize (Hfind x1). - rewrite <- elem_of_list_In in H2x1. - specialize (Hfind H2x1). - intros HContra. subst x. - apply Hfind. - rewrite <- elem_of_list_In in H2x0. - apply H2x0. - } - } - } - } - } - } -Qed. - - +(* Lemma compile_correct_1 {Σ : StaticModel} {Act : Set} @@ -10272,7 +8121,7 @@ Proof. } } Qed. - +*) Definition isDownC {Σ : StaticModel} From 8e794499c60a0bd38c7f5354f408654080f32238 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Sat, 6 Jul 2024 21:24:43 +0200 Subject: [PATCH 3/3] remove stuff --- minuska/_CoqProject | 2 +- minuska/theories/naive_interpreter.v | 4 +- minuska/theories/try_match.v | 1541 -------------------------- 3 files changed, 2 insertions(+), 1545 deletions(-) delete mode 100644 minuska/theories/try_match.v diff --git a/minuska/_CoqProject b/minuska/_CoqProject index 97854213..617f0cde 100644 --- a/minuska/_CoqProject +++ b/minuska/_CoqProject @@ -16,7 +16,7 @@ theories/minuska.v theories/string_variables.v theories/BuiltinValue.v theories/builtins.v -theories/try_match.v +theories/basic_matching.v theories/naive_interpreter.v theories/interpreter_results.v theories/default_static_model.v diff --git a/minuska/theories/naive_interpreter.v b/minuska/theories/naive_interpreter.v index 893a8133..c55558c3 100644 --- a/minuska/theories/naive_interpreter.v +++ b/minuska/theories/naive_interpreter.v @@ -7,8 +7,6 @@ From Minuska Require Import syntax_properties properties spec_interpreter - basic_matching - try_match valuation_merge . @@ -887,7 +885,7 @@ Proof. apply bind_Some_T_2. exists ρ1. split>[apply H3ρ2|]. - unfold matchesb in *; simpl in *. + simpl in *. ltac1:(case_match). { reflexivity. } unfold satisfies in H2; simpl in H2. diff --git a/minuska/theories/try_match.v b/minuska/theories/try_match.v deleted file mode 100644 index 006283d0..00000000 --- a/minuska/theories/try_match.v +++ /dev/null @@ -1,1541 +0,0 @@ -From Minuska Require Import - prelude - spec - lowlang - syntax_properties - properties - semantics_properties - basic_matching -. - - -Definition use_left -{Σ : StaticModel} -(og1 og2: option GroundTerm): option GroundTerm := -match og1, og2 with -| None, None => None -| Some g1, None => Some g1 -| None, Some g2 => Some g2 -| Some g1, Some g2 => Some g1 -end. - -Definition valuations_compatible - {Σ : StaticModel} - (ρ1 ρ2 : Valuation) : bool - := forallb (fun k => bool_decide (ρ1 !! k = ρ2 !! k)) (elements (dom ρ1 ∩ dom ρ2)) -. - -Definition merge_valuations - {Σ : StaticModel} - (ρ1 ρ2 : Valuation) - : option Valuation := -if (valuations_compatible ρ1 ρ2) -then - Some (merge use_left ρ1 ρ2) -else - None -. - -Lemma merge_valuations_correct - {Σ : StaticModel} - (ρ1 ρ2 ρ : Valuation): - merge_valuations ρ1 ρ2 = Some ρ -> - ρ1 ⊆ ρ /\ - ρ2 ⊆ ρ -. -Proof. - unfold Valuation in *. - unfold merge_valuations. - unfold is_left. - destruct ((valuations_compatible ρ1 ρ2)) eqn:Hcompat; intros H. - { - inversion H; subst; clear H. - unfold valuations_compatible in Hcompat. - unfold is_true in Hcompat. - rewrite forallb_forall in Hcompat; cbn. - ltac1:(setoid_rewrite <- elem_of_list_In in Hcompat). - ltac1:(setoid_rewrite elem_of_elements in Hcompat). - split; intros i; - destruct (ρ1 !! i) eqn:Hρ1i; - destruct (ρ2 !! i) eqn:Hρ2i; - destruct (merge use_left ρ1 ρ2 !! i) eqn:Hmergei; - simpl; - try (exact I); - ltac1:(rewrite lookup_merge in Hmergei); - unfold diag_None in Hmergei; - specialize (Hcompat i); - ltac1:(rewrite Hρ1i in Hmergei); - ltac1:(rewrite Hρ2i in Hmergei); - unfold use_left in Hmergei; - ltac1:(simplify_eq /=); - try reflexivity - . - - ltac1:(ospecialize (Hcompat _)). - { - rewrite elem_of_intersection. - do 2 ltac1:(rewrite elem_of_dom). - split; eexists. - { - apply Hρ1i. - } - { - apply Hρ2i. - } - } - apply bool_decide_eq_true_1 in Hcompat. - unfold Valuation in *. - rewrite Hcompat in Hρ1i. - rewrite Hρ1i in Hρ2i. - ltac1:(congruence). - } - { - inversion H. - } -Qed. - -Lemma merge_valuations_empty_r - {Σ : StaticModel} x - : - merge_valuations x ∅ = Some x -. -Proof. - unfold merge_valuations. - ltac1:(case_match). - { - clear H. - apply f_equal. - rewrite <- merge_Some. - intros i. - unfold use_left. - ltac1:(case_match). - { - ltac1:(rewrite lookup_empty). - reflexivity. - } - { - ltac1:(rewrite lookup_empty). - reflexivity. - } - reflexivity. - } - { - unfold is_left in H. - unfold Valuation in *. - unfold valuations_compatible in H. - rewrite <- not_true_iff_false in H. - ltac1:(exfalso). apply H. clear H. - rewrite forallb_forall. - intros x0 Hx0. - rewrite bool_decide_eq_true. - rewrite <- elem_of_list_In in Hx0. - rewrite elem_of_elements in Hx0. - rewrite elem_of_intersection in Hx0. - destruct Hx0 as [H1 H2]. - ltac1:(exfalso). - ltac1:(rewrite dom_empty in H2). - rewrite elem_of_empty in H2. - inversion H2. - } -Qed. - -Lemma merge_valuations_empty_l - {Σ : StaticModel} x: - merge_valuations ∅ x = Some x -. -Proof. - unfold merge_valuations. - ltac1:(case_match). - { - clear H. - apply f_equal. - rewrite <- merge_Some. - intros i. - unfold use_left. - repeat ltac1:(case_match); - try reflexivity. - { - ltac1:(rewrite lookup_empty in H). - inversion H. - } - { - ltac1:(rewrite lookup_empty in H). - inversion H. - } - reflexivity. - } - { - unfold is_left in H. - unfold Valuation in *. - unfold valuations_compatible in H. - rewrite <- not_true_iff_false in H. - ltac1:(exfalso). apply H. clear H. - rewrite forallb_forall. - intros x0 Hx0. - rewrite bool_decide_eq_true. - rewrite <- elem_of_list_In in Hx0. - rewrite elem_of_elements in Hx0. - rewrite elem_of_intersection in Hx0. - destruct Hx0 as [H1 H2]. - ltac1:(exfalso). - ltac1:(rewrite dom_empty in H1). - rewrite elem_of_empty in H1. - inversion H1. - } -Qed. - - -Lemma merge_use_left_subseteq - {Σ : StaticModel} - (ρ1 ρ2 : Valuation): - ρ1 ⊆ ρ2 -> - merge use_left ρ1 ρ2 = ρ2 -. -Proof. - unfold subseteq. simpl. - unfold Subseteq_Valuation. - unfold Valuation in *. simpl. - unfold map_subseteq. - unfold map_included. - unfold map_relation. - unfold option_relation. - intros H. - apply map_subseteq_po. - { - unfold Valuation. - rewrite map_subseteq_spec. - intros i x Hix. - rewrite lookup_merge in Hix. - unfold diag_None in Hix. - unfold use_left in Hix. - ltac1:(repeat case_match; simplify_eq/=; try reflexivity). - { - specialize (H i). - rewrite H0 in H. - rewrite H1 in H. - subst. - reflexivity. - } - { - specialize (H i). - rewrite H0 in H. - rewrite H1 in H. - inversion H. - } - } - { - unfold Valuation. - rewrite map_subseteq_spec. - intros i x Hix. - rewrite lookup_merge. - unfold diag_None. - unfold use_left. - ltac1:(repeat case_match; simplify_eq/=; try reflexivity). - specialize (H i). - rewrite H1 in H. - rewrite H0 in H. - subst. - reflexivity. - } -Qed. - - -Lemma merge_valuations_dom - {Σ : StaticModel} - (ρ1 ρ2 ρ : Valuation): - merge_valuations ρ1 ρ2 = Some ρ -> - dom ρ = dom ρ1 ∪ dom ρ2 -. -Proof. - assert (Hm := merge_valuations_correct ρ1 ρ2 ρ). - unfold merge_valuations in *. - destruct ((valuations_compatible ρ1 ρ2)); simpl in *; - intros H; inversion H; subst; clear H. - apply leibniz_equiv. - rewrite set_equiv_subseteq. - split. - { - clear Hm. - rewrite elem_of_subseteq. - intros x Hx. - unfold Valuation in *. - rewrite elem_of_dom in Hx. - rewrite elem_of_union. - rewrite elem_of_dom. - rewrite elem_of_dom. - destruct Hx as [y Hy]. - rewrite lookup_merge in Hy. - unfold diag_None, use_left in Hy. - ltac1:(repeat case_match; simplify_eq/=); - unfold is_Some. - { - left; eexists; reflexivity. - } - { - left; eexists; reflexivity. - } - { - right; eexists; reflexivity. - } - } - { - specialize (Hm eq_refl). - destruct Hm as [Hm1 Hm2]. - rewrite union_subseteq. - rewrite elem_of_subseteq. - rewrite elem_of_subseteq. - unfold Valuation in *. - split; intros x Hx; rewrite elem_of_dom in Hx; - destruct Hx as [y Hy]; rewrite elem_of_dom; - exists y; eapply lookup_weaken>[apply Hy|]; - assumption. - } -Qed. - - -Lemma omap_Some - {Σ : StaticModel} - (ρ : Valuation): - omap [eta Some] ρ = ρ -. -Proof. - rewrite <- map_fmap_alt. - rewrite map_fmap_id. - reflexivity. -Qed. - -Class TryMatch - {Σ : StaticModel} - (A B : Type) - {_VB: VarsOf B variable} - {_SAB : Satisfies Valuation A B variable} - {_MAB : Matches A B variable} - := -{ - try_match : - A -> B -> option Valuation ; - - try_match_correct : - ∀ (a : A) (b : B) (ρ : Valuation), - try_match a b = Some ρ -> - matchesb ρ a b = true ; - - try_match_complete : - ∀ (a : A) (b : B) (ρ : Valuation), - matchesb ρ a b = true -> - { ρ' : Valuation & - vars_of ρ' = vars_of b /\ - ρ' ⊆ ρ /\ - try_match a b = Some ρ' - } ; - - (* It does not invent variables out of thin air *) - try_match_noOOTA : - ∀ (a : A) (b : B) (ρ : Valuation), - try_match a b = Some ρ -> - vars_of ρ ⊆ vars_of b -}. - - -Arguments try_match : simpl never. - -Fixpoint ApppliedOperator'_try_match_PreTerm' - {Σ : StaticModel} - {Operand1 Operand2 : Type} - {_VOperand2 : VarsOf Operand2 variable} - {_S0 : Satisfies Valuation (Operand1) Operand2 variable} - {_M0 : Matches (Operand1) Operand2 variable} - {_TM0 : TryMatch Operand1 Operand2} - {_S1 : Satisfies Valuation (Operand1) (PreTerm' symbol Operand2) variable} - {_M1 : Matches (Operand1) (PreTerm' symbol Operand2) variable} - {_TM1 : TryMatch Operand1 (PreTerm' symbol Operand2)} - {_S2 : Satisfies Valuation ((PreTerm' symbol Operand1)) Operand2 variable} - {_M2 : Matches ((PreTerm' symbol Operand1)) Operand2 variable} - {_TM2 : TryMatch (PreTerm' symbol Operand1) Operand2} - (x : PreTerm' symbol Operand1) - (y : PreTerm' symbol Operand2) - : - option Valuation -:= -match x, y with -| pt_operator a1, pt_operator a2 => - if decide (a1 = a2) then Some ∅ else None -| pt_operator _, pt_app_operand _ _ => None -| pt_operator _, pt_app_ao _ _ => None -| pt_app_operand _ _ , pt_operator _ => None -| pt_app_operand app1 o1, pt_app_operand app2 o2 => - ρ1 ← ApppliedOperator'_try_match_PreTerm' - app1 - app2; - ρ2 ← try_match o1 o2; - merge_valuations ρ1 ρ2 - -| pt_app_operand app1 o1, pt_app_ao app2 o2 => - ρ1 ← ApppliedOperator'_try_match_PreTerm' - app1 - app2 ; - ρ2 ← try_match o1 o2; - merge_valuations ρ1 ρ2 - -(* TODO? *) -| pt_app_ao app1 o1, pt_operator _ => None - -| pt_app_ao app1 o1, pt_app_operand app2 o2 => - ρ1 ← ApppliedOperator'_try_match_PreTerm' - app1 - app2 ; - ρ2 ← try_match o1 o2; - merge_valuations ρ1 ρ2 - -| pt_app_ao app1 o1, pt_app_ao app2 o2 => - ρ1 ← ApppliedOperator'_try_match_PreTerm' - app1 - app2 ; - ρ2 ← ApppliedOperator'_try_match_PreTerm' - o1 - o2 ; - merge_valuations ρ1 ρ2 -end. - -(* - Note: I think that this lemma needs to be formulated in this - generalized way, with two valuations related by inclusion. - The interface, as represented by the `TryMatch` class, - hides this detail. -*) -Lemma ApppliedOperator'_try_match_PreTerm'_correct - {Σ : StaticModel} - {Operand1 Operand2 : Type} - {_VOperand1 : VarsOf Operand1 variable} - {_VOperand2 : VarsOf Operand2 variable} - {_S0 : Satisfies Valuation (Operand1) Operand2 variable} - {_S0P : SatisfiesProperties Valuation (Operand1) Operand2 variable} - {_M0 : Matches (Operand1) Operand2 variable} - {_TM0 : TryMatch Operand1 Operand2} - {_S1 : Satisfies Valuation (Operand1) (PreTerm' symbol Operand2) variable} - {_SP1 : SatisfiesProperties Valuation (Operand1) (PreTerm' symbol Operand2) variable} - {_M1 : Matches (Operand1) (PreTerm' symbol Operand2) variable} - {_TM1 : TryMatch Operand1 (PreTerm' symbol Operand2)} - {_S2 : Satisfies Valuation ((PreTerm' symbol Operand1)) Operand2 variable} - {_S2P : SatisfiesProperties Valuation ((PreTerm' symbol Operand1)) Operand2 variable} - {_M2 : Matches ((PreTerm' symbol Operand1)) Operand2 variable} - {_TM2 : TryMatch (PreTerm' symbol Operand1) Operand2} - (ρ ρ' : Valuation) - (a : PreTerm' symbol Operand1) - (b : PreTerm' symbol Operand2) - : - ρ ⊆ ρ' -> - ApppliedOperator'_try_match_PreTerm' a b = Some ρ -> - matchesb ρ' a b = true -. -Proof. - revert b ρ ρ'. - induction a; intros b' ρ ρ' HH H; destruct b'; cbn in *; intros. - { - intros. - unfold is_left in *. - unfold decide,bool_decide in *. - repeat ltac1:(case_match); subst; simpl; - try reflexivity; try ltac1:(congruence). - { - ltac1:(simplify_eq/=). - unfold matchesb. simpl. - unfold bool_decide; ltac1:(case_match); subst; - ltac1:(congruence). - } - } - { - inversion H. - } - { - inversion H. - } - { - inversion H. - } - { - rewrite bind_Some in H. - destruct H as [x [H21 H22]]. - rewrite bind_Some in H22. - destruct H22 as [x0 [H221 H222]]. - - - assert (H221' := H221). - apply try_match_correct in H221. - assert (H222' := H222). - apply merge_valuations_correct in H222'. - destruct H222' as [Hsub1 Hsub2]. - - assert (IH := IHa _ _ _ Hsub1 H21). - unfold matchesb; simpl. - unfold Valuation in *. - apply matchesb_ext with (v2 := ρ') in IH - >[|apply _| assumption]. - unfold matchesb in IH; simpl in IH. - rewrite IH; simpl. - eapply matchesb_ext in H221>[|apply _| apply Hsub2]. - eapply matchesb_ext in H221>[|apply _| apply HH]. - assumption. - } - { - rewrite bind_Some in H. - destruct H as [x [H21 H22]]. - unfold matchesb; simpl. - rewrite bind_Some in H22. - destruct H22 as [x0 [Hx01 Hx02]]. - apply merge_valuations_correct in Hx02. - apply try_match_correct in Hx01. - eapply matchesb_ext in Hx01>[|apply _| apply Hx02]. - eapply matchesb_ext in Hx01>[|apply _| apply HH]. - rewrite Hx01. - eapply IHa in H21>[|apply Hx02]. - eapply matchesb_ext in H21>[|apply _| apply HH]. - unfold matchesb in H21; simpl in H21. - rewrite H21. - reflexivity. - } - { - inversion H. - } - { - rewrite bind_Some in H. - destruct H as [x [H21 H22]]. - rewrite bind_Some in H22. - destruct H22 as [x0 [H221 H222]]. - apply merge_valuations_correct in H222. - destruct H222 as [Hxρ Hx0ρ]. - unfold matchesb; simpl. - - assert (IH1 := IHa1 _ _ _ Hxρ H21). - apply matchesb_ext with (v2 := ρ') in IH1>[|apply _| assumption]. - unfold matchesb in IH1; simpl in IH1. - rewrite IH1; simpl. - - apply try_match_correct in H221. - eapply matchesb_ext in H221>[|apply _| apply Hx0ρ]. - eapply matchesb_ext in H221>[|apply _| apply HH]. - exact H221. - } - { - rewrite bind_Some in H. - destruct H as [x [H21 H22]]. - rewrite bind_Some in H22. - destruct H22 as [x0 [H221 H222]]. - assert (Hsub := H222). - apply merge_valuations_correct in Hsub. - destruct Hsub as [Hsub1 Hsub2]. - - - unfold matchesb; simpl. - eapply IHa1 in H21>[|apply Hsub1]. - eapply IHa2 in H221>[|apply Hsub2]. - eapply matchesb_ext in H21>[|apply _| apply HH]. - eapply matchesb_ext in H221>[|apply _| apply HH]. - unfold matchesb in H21,H221. simpl in H21,H221. - rewrite H21. rewrite H221. - reflexivity. - } -Qed. - -(* - I define this here only for Valuations - to behave extensionaly. -*) -#[local] -Instance GTEquiv {Σ : StaticModel} - : Equiv GroundTerm := (=). - -#[local] -Instance GTLeibnizEquiv {Σ : StaticModel} - : LeibnizEquiv GroundTerm. -Proof. - intros x y H. apply H. -Qed. - -Lemma dom_merge_use_left - {Σ : StaticModel} - (ρ' ρ'' : Valuation) - : - dom (merge use_left ρ' ρ'') = dom ρ'' ∪ dom ρ' -. -Proof. - unfold Valuation in *. - apply set_eq. - intros x. - rewrite elem_of_dom. - unfold is_Some. - rewrite lookup_merge. - unfold diag_None. - destruct (ρ' !! x) eqn:Heq1,(ρ'' !! x) eqn:Heq2; simpl. - { - split; intros H. - { - destruct H as [x' Hx']. - inversion Hx'; subst; clear Hx'. - rewrite elem_of_union. - left. - rewrite elem_of_dom. - exists g0. assumption. - } - { - eexists. reflexivity. - } - } - { - split; intros H. - { - rewrite elem_of_union. - right. - rewrite elem_of_dom. - exists g. - assumption. - } - { - eexists. reflexivity. - } - } - { - split; intros H. - { - rewrite elem_of_union. - left. - rewrite elem_of_dom. - exists g. - assumption. - } - { - eexists. reflexivity. - } - } - { - split; intros H. - { - destruct H as [x' Hx']. - inversion Hx'. - } - { - rewrite elem_of_union in H. - destruct H as [H|H]. - { - rewrite elem_of_dom in H. - destruct H as [g Hg]. - ltac1:(simplify_eq/=). - } - { - rewrite elem_of_dom in H. - destruct H as [g Hg]. - ltac1:(simplify_eq/=). - } - } - } -Qed. - -Lemma merge_use_left_below {Σ : StaticModel} (ρ ρ' ρ'': Valuation) : - ρ' ⊆ ρ -> - ρ'' ⊆ ρ -> - merge use_left ρ' ρ'' ⊆ ρ -. -Proof. - intros H1 H2. - unfold Valuation in *. - apply map_subseteq_spec. - intros i x Hix. - rewrite lookup_merge in Hix. - unfold diag_None, use_left in Hix. - ltac1:(repeat case_match; simplify_eq/=). - { - eapply lookup_weaken. - { apply H. } - { assumption. } - } - { - eapply lookup_weaken. - { apply H. } - { assumption. } - } - { - eapply lookup_weaken. - { apply H0. } - { assumption. } - } -Qed. - -Lemma ApppliedOperator'_try_match_PreTerm'_complete - {Σ : StaticModel} - {Operand1 Operand2 : Type} - {_VOperand1 : VarsOf Operand1 variable} - {_VOperand2 : VarsOf Operand2 variable} - {_S0 : Satisfies Valuation (Operand1) Operand2 variable} - {_M0 : Matches (Operand1) Operand2 variable} - {_TM0 : TryMatch Operand1 Operand2} - {_S1 : Satisfies Valuation (Operand1) (PreTerm' symbol Operand2) variable} - {_M1 : Matches (Operand1) (PreTerm' symbol Operand2) variable} - {_TM1 : TryMatch Operand1 (PreTerm' symbol Operand2)} - {_S2 : Satisfies Valuation ((PreTerm' symbol Operand1)) Operand2 variable} - {_M2 : Matches ((PreTerm' symbol Operand1)) Operand2 variable} - {_TM2 : TryMatch (PreTerm' symbol Operand1) Operand2} - (ρ : Valuation) - (a : PreTerm' symbol Operand1) - (b : PreTerm' symbol Operand2) - : - matchesb ρ a b = true -> - { ρ' : _ & - vars_of ρ' = vars_of b /\ - ρ' ⊆ ρ /\ - ApppliedOperator'_try_match_PreTerm' a b = Some ρ' - } -. -Proof. - unfold Valuation in *. - revert ρ b. - induction a; intros ρ b''. - { - (*subst f.*) - unfold matchesb; simpl. - unfold decide,decide_rel,is_left,bool_decide. - repeat ltac1:(case_match); subst; - intros H; try (ltac1:(congruence)). - - clear H. - cbn. - exists ∅. - cbn. - repeat split. - unfold Valuation in *. - apply map_empty_subseteq. - } - { - cbn. - destruct b''. - { - intros H; inversion H. - } - { - intros H. - unfold matchesb in H. - simpl in H. - rewrite andb_true_iff in H. - destruct H as [H1 H2]. - specialize (IHa ρ b'' H1). - destruct IHa as [ρ' [IH0 [IH1 IH2]]]. - apply try_match_complete in H2. - destruct H2 as [ρ'' [Hρ''0 [Hρ''1 Hρ''2]]]. - rewrite IH2. - cbn. - rewrite Hρ''2. - cbn. - - exists (merge use_left ρ' ρ''). - split. - { - unfold vars_of; simpl. - rewrite <- Hρ''0. - unfold vars_of in IH0. simpl in IH0. - rewrite <- IH0. - unfold Valuation in *. - rewrite dom_merge_use_left. - clear. - ltac1:(set_solver). - } - split. - { - apply merge_use_left_below; assumption. - } - { - unfold merge_valuations. - ltac1:(case_match). - { - reflexivity. - } - { - ltac1:(exfalso). - rewrite <- not_true_iff_false in H. - apply H. clear H. - unfold valuations_compatible. - unfold is_true. - rewrite forallb_forall. - intros x Hx. - apply bool_decide_eq_true. - apply elem_of_list_In in Hx. - rewrite elem_of_elements in Hx. - rewrite elem_of_intersection in Hx. - destruct Hx as [Hxρ' Hxρ'']. - unfold Valuation in *. - rewrite elem_of_dom in Hxρ'. - rewrite elem_of_dom in Hxρ''. - destruct Hxρ' as [g1 Hg1]. - destruct Hxρ'' as [g2 Hg2]. - rewrite Hg1. - rewrite Hg2. - apply f_equal. - apply lookup_weaken with (m2 := ρ) in Hg1>[|assumption]. - apply lookup_weaken with (m2 := ρ) in Hg2>[|assumption]. - ltac1:(simplify_eq/=). - reflexivity. - } - } - } - { - intros H. - unfold matchesb in H. - simpl in H. - rewrite andb_true_iff in H. - destruct H as [H1 H2]. - specialize (IHa ρ _ H1). - destruct IHa as [ρ' [IH0 [IH1 IH2]]]. - apply try_match_complete in H2. - destruct H2 as [ρ'' [Hρ''0 [Hρ''1 Hρ''2]]]. - rewrite IH2. - cbn. - rewrite Hρ''2. - cbn. - - exists (merge use_left ρ' ρ''). - split. - { - unfold vars_of in Hρ''0. simpl in Hρ''0. - unfold vars_of; simpl. - rewrite <- Hρ''0. - unfold vars_of in IH0. simpl in IH0. - rewrite <- IH0. - unfold Valuation in *. - rewrite dom_merge_use_left. - clear. - ltac1:(set_solver). - } - split. - { - apply merge_use_left_below; assumption. - } - { - unfold merge_valuations. - ltac1:(case_match). - { - reflexivity. - } - { - ltac1:(exfalso). - rewrite <- not_true_iff_false in H. - apply H. clear H. - unfold valuations_compatible. - unfold is_true. - rewrite forallb_forall. - intros x Hx. - apply bool_decide_eq_true. - apply elem_of_list_In in Hx. - rewrite elem_of_elements in Hx. - rewrite elem_of_intersection in Hx. - destruct Hx as [Hxρ' Hxρ'']. - unfold Valuation in *. - rewrite elem_of_dom in Hxρ'. - rewrite elem_of_dom in Hxρ''. - destruct Hxρ' as [g1 Hg1]. - destruct Hxρ'' as [g2 Hg2]. - rewrite Hg1. - rewrite Hg2. - apply f_equal. - apply lookup_weaken with (m2 := ρ) in Hg1>[|assumption]. - apply lookup_weaken with (m2 := ρ) in Hg2>[|assumption]. - ltac1:(simplify_eq/=). - reflexivity. - } - } - } - } - { - cbn. - destruct b''. - { - intros H; inversion H. - } - { - intros H. - unfold matchesb in H. - simpl in H. - rewrite andb_true_iff in H. - destruct H as [H1 H2]. - unfold Valuation in *. - specialize (IHa1 _ _ H1). - - destruct IHa1 as [ρ' [IH0 [IH1 IH2]]]. - apply try_match_complete in H2. - destruct H2 as [ρ'' [Hρ''0 [Hρ''1 Hρ''2]]]. - rewrite IH2. - cbn. - rewrite Hρ''2. - cbn. - - exists (merge use_left ρ' ρ''). - split. - { - unfold vars_of; simpl. - rewrite <- Hρ''0. - unfold vars_of in IH0. simpl in IH0. - rewrite <- IH0. - unfold Valuation in *. - rewrite dom_merge_use_left. - clear. - ltac1:(set_solver). - } - split. - { - apply merge_use_left_below; assumption. - } - { - unfold merge_valuations. - ltac1:(case_match). - { - reflexivity. - } - { - ltac1:(exfalso). - rewrite <- not_true_iff_false in H. - apply H. clear H. - unfold valuations_compatible. - unfold is_true. - rewrite forallb_forall. - intros x Hx. - apply bool_decide_eq_true. - apply elem_of_list_In in Hx. - rewrite elem_of_elements in Hx. - rewrite elem_of_intersection in Hx. - destruct Hx as [Hxρ' Hxρ'']. - unfold Valuation in *. - rewrite elem_of_dom in Hxρ'. - rewrite elem_of_dom in Hxρ''. - destruct Hxρ' as [g1 Hg1]. - destruct Hxρ'' as [g2 Hg2]. - rewrite Hg1. - rewrite Hg2. - apply f_equal. - apply lookup_weaken with (m2 := ρ) in Hg1>[|assumption]. - apply lookup_weaken with (m2 := ρ) in Hg2>[|assumption]. - ltac1:(simplify_eq/=). - reflexivity. - } - } - } - { - intros H. - unfold matchesb in H. - simpl in H. - rewrite andb_true_iff in H. - destruct H as [H1 H2]. - specialize (IHa1 _ _ H1). - specialize (IHa2 _ _ H2). - destruct IHa1 as [ρ1' [IH10 [IH11 IH12]]]. - destruct IHa2 as [ρ2' [IH20 [IH21 IH22]]]. - - exists (merge use_left ρ1' ρ2'). - split. - { - unfold vars_of in *|-. simpl in *|-. - simpl. - unfold vars_of; simpl. - rewrite <- IH10. - rewrite <- IH20. - unfold Valuation in *. - rewrite dom_merge_use_left. - clear. - ltac1:(set_solver). - } - split. - { - apply merge_use_left_below; assumption. - } - { - rewrite bind_Some. - eexists. - split>[apply IH12|]. - rewrite bind_Some. - eexists. - split>[apply IH22|]. - unfold merge_valuations. - ltac1:(case_match). - { - reflexivity. - } - { - ltac1:(exfalso). - rewrite <- not_true_iff_false in H. - apply H. clear H. - unfold valuations_compatible. - unfold is_true. - rewrite forallb_forall. - intros x Hx. - apply bool_decide_eq_true. - apply elem_of_list_In in Hx. - rewrite elem_of_elements in Hx. - rewrite elem_of_intersection in Hx. - destruct Hx as [Hxρ' Hxρ'']. - unfold Valuation in *. - rewrite elem_of_dom in Hxρ'. - rewrite elem_of_dom in Hxρ''. - destruct Hxρ' as [g1 Hg1]. - destruct Hxρ'' as [g2 Hg2]. - rewrite Hg1. - rewrite Hg2. - apply f_equal. - apply lookup_weaken with (m2 := ρ) in Hg1>[|assumption]. - apply lookup_weaken with (m2 := ρ) in Hg2>[|assumption]. - ltac1:(simplify_eq/=). - reflexivity. - } - } - } - } -Qed. - -#[export] -Program Instance TryMatch_PreTerm' - {Σ : StaticModel} - {Operand1 Operand2 : Type} - {_VOperand1 : VarsOf Operand1 variable} - {_VOperand2 : VarsOf Operand2 variable} - {_S0 : Satisfies Valuation (Operand1) Operand2 variable} - {_SP0 : SatisfiesProperties Valuation (Operand1) Operand2 variable} - {_M0 : Matches (Operand1) Operand2 variable} - {_TM0 : TryMatch Operand1 Operand2} - {_S1 : Satisfies Valuation (Operand1) (PreTerm' symbol Operand2) variable} - {_SP1 : SatisfiesProperties Valuation (Operand1) (PreTerm' symbol Operand2) variable} - {_M1 : Matches (Operand1) (PreTerm' symbol Operand2) variable} - {_TM1 : TryMatch Operand1 (PreTerm' symbol Operand2)} - {_S2 : Satisfies Valuation ((PreTerm' symbol Operand1)) Operand2 variable} - {_SP2 : SatisfiesProperties Valuation ((PreTerm' symbol Operand1)) Operand2 variable} - {_M2 : Matches ((PreTerm' symbol Operand1)) Operand2 variable} - {_TM2 : TryMatch (PreTerm' symbol Operand1) Operand2} -: - TryMatch (PreTerm' symbol Operand1) (PreTerm' symbol Operand2) -:= {| - try_match := ApppliedOperator'_try_match_PreTerm' ; - try_match_correct := _; - try_match_complete := _; -|}. -Next Obligation. - intros. - apply ApppliedOperator'_try_match_PreTerm'_correct with (ρ := ρ). - { - unfold Valuation in *. - apply reflexivity. - } - { apply H. } -Qed. -Next Obligation. - intros. - apply ApppliedOperator'_try_match_PreTerm'_complete. - assumption. -Qed. -Next Obligation. - intros. ltac1:(rename H0 into Hx). - revert a ρ H x Hx. - induction b; unfold vars_of; simpl in *; intros a' ρ' H' x Hx. - { - destruct a'; simpl in *; ltac1:(repeat case_match; simplify_eq/=). - ltac1:(rewrite dom_empty_L in Hx). - exact Hx. - } - { - destruct a'; simpl in *; ltac1:(simplify_eq/=). - { - rewrite bind_Some in H'. - destruct H' as [x0 [H1x0 H2x0]]. - rewrite bind_Some in H2x0. - destruct H2x0 as [x1 [H1x1 H2x1]]. - assert (H2x1' := H2x1). - apply merge_valuations_dom in H2x1'. - unfold Valuation in *. - rewrite H2x1' in Hx. - rewrite elem_of_union in Hx. - destruct Hx as [H|H]. - { - specialize (IHb a' x0 H1x0 x H). - rewrite elem_of_union. - right. apply IHb. - } - { - apply try_match_noOOTA in H1x1. - clear - H1x1 H. - ltac1:(set_solver). - } - } - { - rewrite bind_Some in H'. - destruct H' as [x0 [H1x0 H2x0]]. - rewrite bind_Some in H2x0. - destruct H2x0 as [x1 [H1x1 H2x1]]. - assert (H2x1' := H2x1). - apply merge_valuations_dom in H2x1'. - unfold Valuation in *. - rewrite H2x1' in Hx. - rewrite elem_of_union in Hx. - destruct Hx as [H|H]. - { - assert (IH := IHb a'1). - specialize (IH x0 H1x0 x H). - rewrite elem_of_union. - right. apply IH. - } - { - apply try_match_noOOTA in H1x1. - clear - H1x1 H. - ltac1:(set_solver). - } - } - } - { - destruct a'; simpl in *; ltac1:(simplify_eq/=). - { - rewrite bind_Some in H'. - destruct H' as [x0 [H1x0 H2x0]]. - rewrite bind_Some in H2x0. - destruct H2x0 as [x1 [H1x1 H2x1]]. - assert (H2x1' := H2x1). - apply merge_valuations_dom in H2x1'. - unfold Valuation in *. - rewrite H2x1' in Hx. - rewrite elem_of_union in Hx. - destruct Hx as [H|H]. - { - assert (IH1 := IHb1 a'). - specialize (IH1 x0 H1x0 x H). - rewrite elem_of_union. - left. apply IH1. - } - { - apply try_match_noOOTA in H1x1. - clear - H1x1 H. - ltac1:(set_solver). - } - } - { - rewrite bind_Some in H'. - destruct H' as [x0 [H1x0 H2x0]]. - rewrite bind_Some in H2x0. - destruct H2x0 as [x1 [H1x1 H2x1]]. - assert (H2x1' := H2x1). - apply merge_valuations_dom in H2x1'. - unfold Valuation in *. - rewrite H2x1' in Hx. - rewrite elem_of_union in Hx. - destruct Hx as [H|H]. - { - assert (IH1 := IHb1 a'1). - specialize (IH1 _ H1x0 x H). - rewrite elem_of_union. - left. apply IH1. - } - { - assert (IH2 := IHb2 a'2). - specialize (IH2 _ H1x1 x H). - rewrite elem_of_union. - right. apply IH2. - } - } - } -Qed. -Fail Next Obligation. - -Definition ApppliedOperatorOr'_try_match_Term' - {Σ : StaticModel} - {Operand1 Operand2 : Type} - {_V1 : VarsOf Operand1 variable} - {_V2 : VarsOf Operand2 variable} - {_S1 : Satisfies Valuation Operand1 Operand2 variable} - {_SP1 : SatisfiesProperties Valuation Operand1 Operand2 variable} - {_M1 : Matches Operand1 Operand2 variable} - {_TM1 : TryMatch Operand1 Operand2} - {_S2 : Satisfies Valuation Operand1 (PreTerm' symbol Operand2) variable} - {_SP2 : SatisfiesProperties Valuation Operand1 (PreTerm' symbol Operand2) variable} - {_M2 : Matches Operand1 (PreTerm' symbol Operand2) variable} - {_TM2 : TryMatch Operand1 (PreTerm' symbol Operand2)} - {_S3 : Satisfies Valuation (PreTerm' symbol Operand1) Operand2 variable} - {_SP3 : SatisfiesProperties Valuation (PreTerm' symbol Operand1) Operand2 variable} - {_M3 : Matches (PreTerm' symbol Operand1) Operand2 variable} - {_TM3 : TryMatch (PreTerm' symbol Operand1) Operand2} - (x : Term' symbol Operand1) - (y : Term' symbol Operand2) - : option Valuation := -match x, y with -| term_preterm app1, term_preterm app2 => - try_match app1 app2 -| term_preterm app1, term_operand o2 => - try_match app1 o2 -| term_operand o1, term_preterm app2 => - None (* try_match o1 app2 *) -| term_operand o1, term_operand o2 => - try_match o1 o2 -end. - - -#[export] -Program Instance TryMatch_Term' - {Σ : StaticModel} - {Operand1 Operand2 : Type} - {_VOperand1 : VarsOf Operand1 variable} - {_VOperand2 : VarsOf Operand2 variable} - {_S0 : Satisfies Valuation (Operand1) Operand2 variable} - {_SP0 : SatisfiesProperties Valuation (Operand1) Operand2 variable} - {_M0 : Matches (Operand1) Operand2 variable} - {_TM0 : TryMatch Operand1 Operand2} - {_S1 : Satisfies Valuation (Operand1) (PreTerm' symbol Operand2) variable} - {_SP1 : SatisfiesProperties Valuation (Operand1) (PreTerm' symbol Operand2) variable} - {_M1 : Matches (Operand1) (PreTerm' symbol Operand2) variable} - {_TM1 : TryMatch Operand1 (PreTerm' symbol Operand2)} - {_S2 : Satisfies Valuation ((PreTerm' symbol Operand1)) Operand2 variable} - {_SP2 : SatisfiesProperties Valuation ((PreTerm' symbol Operand1)) Operand2 variable} - {_M2 : Matches ((PreTerm' symbol Operand1)) Operand2 variable} - {_TM2 : TryMatch (PreTerm' symbol Operand1) Operand2} -: - TryMatch (Term' symbol Operand1) (Term' symbol Operand2) -:= {| - try_match := ApppliedOperatorOr'_try_match_Term' ; - try_match_correct := _; - try_match_complete := _; -|}. -Next Obligation. - intros. - destruct a,b; simpl in *; unfold matchesb; simpl. - { - apply try_match_correct. apply H. - } - { - apply try_match_correct. apply H. - } - { - inversion H. - } - { - apply try_match_correct. apply H. - } -Qed. -Next Obligation. - intros. - destruct a,b; simpl in *; unfold matchesb in *; simpl in *. - { - apply try_match_complete in H. - assumption. - } - { - apply try_match_complete in H. - assumption. - } - { - inversion H. - } - { - apply try_match_complete in H. - assumption. - } -Qed. -Next Obligation. - intros. - destruct a,b; simpl in *; - unfold vars_of; simpl in *. - { - apply try_match_noOOTA in H. - ltac1:(set_solver). - } - { - apply try_match_noOOTA in H. - ltac1:(set_solver). - } - { inversion H. } - { - apply try_match_noOOTA in H. - ltac1:(set_solver). - } -Qed. -Fail Next Obligation. - - -Definition builtin_value_try_match_BuiltinOrVar - {Σ : StaticModel} - : - builtin_value -> BuiltinOrVar -> option Valuation := -fun b bv => -match bv with -| bov_builtin b' => if (decide (b = b')) then Some ∅ else None -| bov_variable x => Some (<[x := (term_operand b)]>∅) -end. - - -#[export] -Program Instance TryMatch__builtin__BoV - {Σ : StaticModel} -: - TryMatch builtin_value BuiltinOrVar -:= {| - try_match := builtin_value_try_match_BuiltinOrVar ; - try_match_correct := _; - try_match_complete := _; -|}. -Next Obligation. - intros. - destruct b; unfold matchesb; simpl in *. - { - unfold bool_decide. - ltac1:(case_match). - { - apply bool_decide_eq_true in H0. - inversion H; subst; clear H. - ltac1:(case_match);try reflexivity; try ltac1:(contradiction). - } - { - ltac1:(simplify_eq/=). - } - } - { - inversion H; subst; clear H. - unfold Valuation in *. - rewrite lookup_insert. - apply bool_decide_eq_true. - reflexivity. - } -Qed. -Next Obligation. - intros. - unfold Valuation in *. - unfold matchesb in H; destruct b; simpl in H. - { - apply bool_decide_eq_true in H. - subst. simpl. - exists ∅. - split. - { - unfold vars_of; simpl. - unfold Valuation in *. - rewrite dom_empty_L. - reflexivity. - } - split. - { - apply map_empty_subseteq. - } - { - ltac1:(case_match). - { - reflexivity. - } - { - apply bool_decide_eq_false in H. - ltac1:(contradiction). - } - } - } - { - ltac1:(repeat case_match); subst; simpl. - { inversion H. } - { - apply bool_decide_eq_true in H. - subst. - exists (<[x:=term_operand operand]> ∅). - split. - { - unfold vars_of; simpl. - unfold Valuation in *. - rewrite dom_insert_L. - ltac1:(set_solver). - } - split. - { - apply map_subseteq_spec. - intros i x0 Hix0. - destruct (decide (x = i)). - { - subst. - rewrite lookup_insert in Hix0. - inversion Hix0; subst; clear Hix0. - assumption. - } - { - rewrite lookup_insert_ne in Hix0. - { - rewrite lookup_empty in Hix0. - inversion Hix0. - } - { - assumption. - } - } - } - { - reflexivity. - } - } - { - inversion H. - } - } -Qed. -Next Obligation. - intros. ltac1:(rename H0 into Hx). - destruct b; simpl in *. - { - destruct (decide (a = b)); subst; - simpl in *. - { - inversion H; subst; clear H. - apply Hx. - } - { - inversion H. - } - } - { - inversion H; subst; clear H. - unfold vars_of in *; simpl in *. - unfold Valuation in *. - rewrite elem_of_dom in Hx. - destruct Hx as [y Hy]. - destruct (decide (x = x0)). - { - subst. - rewrite lookup_insert in Hy. - rewrite elem_of_singleton. - reflexivity. - } - { - rewrite lookup_insert_ne in Hy. - { - rewrite lookup_empty in Hy. - inversion Hy. - } - { - ltac1:(congruence). - } - } - } -Qed. -Fail Next Obligation. - -Definition pure_GroundTerm_try_match_BuiltinOrVar - {Σ : StaticModel} - : - PreTerm' symbol builtin_value -> - BuiltinOrVar -> - option Valuation -:= fun t bov => -match bov with -| bov_builtin b => None -| bov_variable x => - Some (<[x := (term_preterm t)]>∅) -end. - -#[export] -Program Instance TryMatch__pure_GroundTerm__BoV - {Σ : StaticModel} -: - TryMatch (PreTerm' symbol builtin_value) BuiltinOrVar -:= {| - try_match := pure_GroundTerm_try_match_BuiltinOrVar ; - try_match_correct := _; - try_match_complete := _; -|}. -Next Obligation. - intros. - destruct b; unfold matchesb; simpl in *. - { inversion H. } - { - inversion H; subst; clear H. - apply bool_decide_eq_true. - unfold Valuation in *. - rewrite lookup_insert. - reflexivity. - } -Qed. -Next Obligation. - intros. - unfold Valuation in *. - destruct b; unfold matchesb in H; simpl in *. - { - inversion H. - } - { - apply bool_decide_eq_true in H. - exists (<[x:=term_preterm a]> ∅). - split. - { - unfold vars_of; simpl. - unfold Valuation in *. - rewrite dom_insert_L. - clear. - ltac1:(set_solver). - } - split. - { - apply map_subseteq_spec. - intros i x0 Hix0. - destruct (decide (i = x)). - { - subst. - rewrite lookup_insert in Hix0. - unfold Valuation in *. - inversion Hix0; subst. clear Hix0. - assumption. - } - { - rewrite lookup_insert_ne in Hix0. - { - rewrite lookup_empty in Hix0. - inversion Hix0. - } - { - ltac1:(congruence). - } - } - } - { - reflexivity. - } - } -Qed. -Next Obligation. - intros. ltac1:(rename H0 into Hx). - destruct b; unfold vars_of in *; simpl in *. - { inversion H. } - { - inversion H; subst; clear H. - rewrite elem_of_singleton. - unfold Valuation in *. - rewrite elem_of_dom in Hx. - destruct Hx as [y Hy]. - destruct (decide (x = x0)). - { - subst. - rewrite lookup_insert in Hy. - inversion Hy; subst. reflexivity. - } - { - rewrite lookup_insert_ne in Hy. - rewrite lookup_empty in Hy. - { inversion Hy. } - { ltac1:(congruence). } - } - } -Qed. -Fail Next Obligation. - -#[export] -Program Instance TryMatch__builtin__AO'sB - {Σ : StaticModel} - {B : Type} - {_VB : (VarsOf B variable) } - {_V1 : VarsOf (PreTerm' symbol B) variable} - : - TryMatch builtin_value (PreTerm' symbol B) -:= {| - try_match := fun _ _ => None ; -|}. -Fail Next Obligation. - -#[export] -Instance TryMatch__GroundTerm__SymbolicTerm - {Σ : StaticModel} - : - TryMatch GroundTerm SymbolicTerm -. -Proof. - apply _. -Defined. - -Arguments try_match : simpl never. \ No newline at end of file