(**************************** This file was automatically generated by Rewrite v1.9.0. Brief User Guide to This File In order to understand the main results shown in this file, it is sufficient to consider a few definitions and lemmata, only. We list the most relevant ones below. These form a self-contained part of this file, i.e. there are no references to the other parts, except in the proofs. * terms definition (Search for "Inductive term") This is the set of all terms, inductively defined through constructors. Constructors names are prefixed with h_ to avoid clashes. * term rewriting relation definition (Search for "Inductive R", RC, RCs) We actually define three relations between terms: R, RC, RCS. Given a set of rewriting rules of the form t1 => t2 , R relates all the variable instantiations of t1 and t2 RC is the closure of R under ground term contexts and reflexivity RCs is the reflexive transitive closure of RC . The last one, RCs, is the usual term rewriting relation. * tree automaton (Search for "User Input Automaton") We define the languages for all the automaton states. Their names are prefixed with "O_" to avoid clashes. Note that here we close the languages under intersection contraints and rewritings (RCs). * unreachability results (Search for "Unreachability") These lemmata correspond to the full rules of the form | @a : f(X,...,Y) => @zzResult : !FAIL! . and prove that f(X,...,Y) is indeed not reachable from @a, for all values of X,...,Y. The number of variables X,...,Y can be zero. ****************************) (* Terms, inductively defined through constructors *) Inductive term : Set := | h_ziFAILzi : term | h_0 : term | h_1 : term | h_cons : term -> term -> term | h_failure : term -> term | h_filter : term -> term | h_nil : term | h_tail : term -> term . (* The type of the languages of the automaton states, i.e. a set of terms. *) Definition St := term -> Prop . (**************************** Completed Automaton, with direct transitions removed ****************************) Inductive N_zaziInters : St := with N_zazzzzResult : St := with N_zr0 : St := | T_N_0 : N_zr0 h_1 with N_zr1 : St := | T_N_1 : forall x1 x2, N_zr2 x1 -> N_zaa x2 -> N_zr1 (h_cons x1 x2) | T_N_2 : forall x1, N_zr1 x1 -> N_zr1 (h_failure x1) with N_zr2 : St := | T_N_3 : N_zr2 h_0 with N_zaa : St := | T_N_4 : forall x1 x2, N_zr0 x1 -> N_zr1 x2 -> N_zaa (h_cons x1 x2) | T_N_5 : forall x1 x2, N_zr2 x1 -> N_zaa x2 -> N_zaa (h_cons x1 x2) | T_N_6 : forall x1, N_zaa x1 -> N_zaa (h_failure x1) | T_N_7 : N_zaa h_nil with N_zab : St := (* | T_N_8 : forall x1, N_zr1 x1 -> N_zab x1 *) (* | T_N_9 : forall x1, N_zaa x1 -> N_zab x1 *) | T_N_10 : forall x1 x2, N_zr0 x1 -> N_zr1 x2 -> N_zab (h_cons x1 x2) | T_N_11 : forall x1 x2, N_zr2 x1 -> N_zaa x2 -> N_zab (h_cons x1 x2) | T_N_12 : forall x1, N_zr1 x1 -> N_zab (h_failure x1) | T_N_13 : forall x1, N_zaa x1 -> N_zab (h_failure x1) | T_N_14 : forall x1, N_zS0029 x1 -> N_zab (h_failure x1) | T_N_15 : N_zab h_nil | T_N_16 : forall x1, N_zab x1 -> N_zab (h_tail x1) with N_zac : St := | T_N_17 : forall x1 x2, N_zr2 x1 -> N_zac x2 -> N_zac (h_cons x1 x2) | T_N_18 : forall x1, N_zr1 x1 -> N_zac (h_filter x1) | T_N_19 : forall x1, N_zaa x1 -> N_zac (h_filter x1) | T_N_20 : forall x1, N_zab x1 -> N_zac (h_filter x1) | T_N_21 : N_zac h_nil with N_zS0029 : St := | T_N_22 : forall x1 x2, N_zr2 x1 -> N_zab x2 -> N_zS0029 (h_cons x1 x2) | T_N_23 : forall x1, N_zr1 x1 -> N_zS0029 (h_failure x1) . (* Table of the states of both automata *) Inductive State_N : St -> Prop := | ST_zaziInters : State_N N_zaziInters | ST_zazzzzResult : State_N N_zazzzzResult | ST_zr0 : State_N N_zr0 | ST_zr1 : State_N N_zr1 | ST_zr2 : State_N N_zr2 | ST_zaa : State_N N_zaa | ST_zab : State_N N_zab | ST_zac : State_N N_zac | ST_zS0029 : State_N N_zS0029 . Ltac knownState := match goal with | |- State_N _ => solve [ apply ST_zaziInters | apply ST_zazzzzResult | apply ST_zr0 | apply ST_zr1 | apply ST_zr2 | apply ST_zaa | apply ST_zab | apply ST_zac | apply ST_zS0029 ] end . Ltac apply_transitionsN_tac tac := intros ; try assumption ; first [ apply T_N_0 ; try assumption ; tac | apply T_N_1 ; try assumption ; tac | apply T_N_10 ; try assumption ; tac | apply T_N_11 ; try assumption ; tac | apply T_N_12 ; try assumption ; tac | apply T_N_13 ; try assumption ; tac | apply T_N_14 ; try assumption ; tac | apply T_N_15 ; try assumption ; tac | apply T_N_16 ; try assumption ; tac | apply T_N_17 ; try assumption ; tac | apply T_N_18 ; try assumption ; tac | apply T_N_19 ; try assumption ; tac | apply T_N_2 ; try assumption ; tac | apply T_N_20 ; try assumption ; tac | apply T_N_21 ; try assumption ; tac | apply T_N_22 ; try assumption ; tac | apply T_N_23 ; try assumption ; tac | apply T_N_3 ; try assumption ; tac | apply T_N_4 ; try assumption ; tac | apply T_N_5 ; try assumption ; tac | apply T_N_6 ; try assumption ; tac | apply T_N_7 ; try assumption ; tac ] . Ltac apply_transitionsN_once := apply_transitionsN_tac fail . Ltac apply_transitionsN_rec := idtac ; apply_transitionsN_tac apply_transitionsN_rec . Ltac decomposition_once := match goal with | h : ?s (?f _) |- _ => inversion_clear h ; subst | h : ?s (?f _ _) |- _ => inversion_clear h ; subst (* Here ?x can be either a constant or a variable (representing a Label). A constant could not match with ?s, so we try inversion. *) | h : ?s ?x |- _ => inversion h ; fail end . Ltac decomposition := repeat decomposition_once . (**************************** Rewriting Relation, _not_ closed under contexts ****************************) Inductive R : term -> term -> Prop := | R_1 : R (h_filter (h_nil)) (h_nil) | R_2 : forall V_X , R (h_filter (h_cons V_X (h_nil))) (h_nil) | R_3 : forall V_X V_Xs , R (h_filter (h_cons V_X (h_cons V_X V_Xs))) (h_cons V_X (h_filter (h_cons V_X V_Xs))) | R_4 : forall V_Xs , R (h_filter (h_cons (h_0) (h_cons (h_1) V_Xs))) (h_filter (h_cons (h_1) V_Xs)) | R_5 : forall V_Xs , R (h_filter (h_cons (h_1) (h_cons (h_0) V_Xs))) (h_filter (h_cons (h_0) V_Xs)) | R_6 : forall V_X V_Xs , R (h_tail (h_cons V_X V_Xs)) V_Xs | R_7 : forall V_X , R (h_cons (h_0) (h_cons (h_1) V_X)) (h_failure (h_cons (h_0) (h_cons (h_1) V_X))) (* Full rule handled later *) . Inductive disj : St -> St -> Prop := | D_24 : disj N_zaziInters N_zazzzzResult | D_25 : disj N_zaziInters N_zr0 | D_26 : disj N_zaziInters N_zr1 | D_27 : disj N_zaziInters N_zr2 | D_28 : disj N_zaziInters N_zaa | D_29 : disj N_zaziInters N_zab | D_30 : disj N_zaziInters N_zac | D_31 : disj N_zaziInters N_zS0029 | D_32 : disj N_zazzzzResult N_zazzzzResult | D_33 : disj N_zazzzzResult N_zr0 | D_34 : disj N_zazzzzResult N_zr1 | D_35 : disj N_zazzzzResult N_zr2 | D_36 : disj N_zazzzzResult N_zaa | D_37 : disj N_zazzzzResult N_zab | D_38 : disj N_zazzzzResult N_zac | D_39 : disj N_zazzzzResult N_zS0029 | D_40 : disj N_zr0 N_zr1 | D_41 : disj N_zr0 N_zr2 | D_42 : disj N_zr0 N_zaa | D_43 : disj N_zr0 N_zab | D_44 : disj N_zr0 N_zac | D_45 : disj N_zr0 N_zS0029 | D_46 : disj N_zr1 N_zr2 | D_47 : disj N_zr2 N_zaa | D_48 : disj N_zr2 N_zab | D_49 : disj N_zr2 N_zac | D_50 : disj N_zr2 N_zS0029 . Ltac disj_table := first [ apply D_24 | apply D_25 | apply D_26 | apply D_27 | apply D_28 | apply D_29 | apply D_30 | apply D_31 | apply D_32 | apply D_33 | apply D_34 | apply D_35 | apply D_36 | apply D_37 | apply D_38 | apply D_39 | apply D_40 | apply D_41 | apply D_42 | apply D_43 | apply D_44 | apply D_45 | apply D_46 | apply D_47 | apply D_48 | apply D_49 | apply D_50 ] . Definition disjoint_on t := forall s1 s2, disj s1 s2 -> s1 t -> s2 t -> False . Ltac disj_app := match goal with | h1 : ?s1 ?t , h2 : ?s2 ?t , h3 : disjoint_on ?t |- _ => apply (h3 s1 s2) ; [ disj_table ; assumption | apply h1 | apply h2 ] end . Lemma disjoint : forall t, disjoint_on t. Proof. intro t ; induction t ; intro s1 ; intro s2 ; intro H ; intros ; (* abstract here reduces proof size & check time *) abstract (inversion H ; subst ; abstract ((decomposition_once ; idtac "decomposed 1st") ; abstract ((decomposition_once ; idtac "decomposed 2nd") ; abstract disj_app ))) . Save. (* Change the goal to False *) Ltac absurdum := cut False ; [ contradiction | idtac ] . Ltac empty_intersection := match goal with | h1 : ?s1 ?t , h2 : ?s2 ?t |- _ => absurdum ; apply (disjoint t s1 s2) ; [ disj_table | try assumption | try assumption ] end . (* After decomposition, for rewritings like f X => X, we might have to prove s1 t -> s2 t, which is not directly possible since we removed these transitions. Here, we need just one more inversion *) Ltac inversionVar := match goal with | h : ?s ?t |- _ ?t => inversion h ; subst | _ => idtac end . Lemma Automaton_N_closed_under_R : forall s_n x y, State_N s_n -> s_n x -> R x y -> s_n y. Proof. intros ; inversion H ; subst ; abstract ( inversion H1 ; subst ; abstract ( decomposition ; inversionVar ; abstract ( apply_transitionsN_rec || empty_intersection ))) . Save. (**************************** Rewriting Relation (closed under contexts and reflexivity). ****************************) Inductive RC : term -> term -> Prop := | RC_S : forall t, RC t t | RC_R : forall t u, R t u -> RC t u | RC_h_cons : forall t1 t2 u1 u2, RC t1 u1 -> RC t2 u2 -> RC (h_cons t1 t2) (h_cons u1 u2) | RC_h_failure : forall t1 u1, RC t1 u1 -> RC (h_failure t1) (h_failure u1) | RC_h_filter : forall t1 u1, RC t1 u1 -> RC (h_filter t1) (h_filter u1) | RC_h_tail : forall t1 u1, RC t1 u1 -> RC (h_tail t1) (h_tail u1) . (**************************** Rewriting Relation (closed under contexts and refl, trans). ****************************) Inductive RCs : term -> term -> Prop := | RCs_S : forall t, RCs t t | RCs_T : forall t1 t2 t3, RCs t1 t2 -> RC t2 t3 -> RCs t1 t3 . Scheme Min_RC := Minimality for RC Sort Prop . Definition rew t u := forall s_n, State_N s_n -> s_n t -> s_n u . (* When (RC t u), (rew t u) and (s t), add (s u) as Hp *) Ltac RC_augment_once := match goal with | h : rew ?t ?u , h2 : ?s ?t |- _ => match goal with | h3 : s u |- _ => fail 1 | _ => cut (s u) ; [ intro | apply (h s) ; [ knownState | exact h2 ] ] end end . Ltac RC_augment := repeat RC_augment_once . Lemma Automaton_N_closed_ctx : forall t u, RC t u -> rew t u . Proof. intros t u H ; apply Min_RC ; solve [ (* RC_S case *) intro ; intro ; intro ; assumption (* RC_R case : use closure lemma *) | intro t0 ; intros ; intro s_t ; intro ; intros ; apply (Automaton_N_closed_under_R s_t t0) ; assumption (* The actual contexts *) | intro ; intros ; intro s_t ; intro S1 ; intros ; inversion S1 ; subst ; decomposition ; RC_augment ; apply_transitionsN_once (* The Min base *) | assumption ] . Save. Lemma Automaton_N_closed_under_RC : forall s_n t u, State_N s_n -> s_n t -> RC t u -> s_n u. Proof. intro s_n ; intros ; cut (rew t u) ; [ intro Rew ; unfold rew in Rew ; apply (Rew s_n) ; assumption | apply Automaton_N_closed_ctx ; assumption ]. Save. Lemma Automaton_N_closed_under_RCs : forall s_n t u, State_N s_n -> s_n t -> RCs t u -> s_n u. Proof. intros ; induction H1 ; [ assumption | apply (Automaton_N_closed_under_RC s_n t2 t3) ; [ assumption | auto | assumption ] ] . Save. (* Intersection Constraints *) Inductive intCon_N : St -> St -> St -> Prop := . Lemma Automaton_N_satisfies_intersection_constraints : forall s1 s2 s3 t, intCon_N s1 s2 s3 -> s2 t -> s3 t -> s1 t . Proof. intros s1 s2 s3 t I S2 S3 ; inversion I ; subst ; inversion S2 ; subst ; decomposition ; (apply_transitionsN_once || empty_intersection). Save. (**************************** The User Input Automaton ****************************) Inductive O_zr0 : St := | T_O_51 : O_zr0 h_1 | T_O_52 : forall t1 t2 , O_zr0 t1 -> RCs t1 t2 -> O_zr0 t2 with O_zr1 : St := | T_O_53 : forall x1 x2, O_zr2 x1 -> O_zaa x2 -> O_zr1 (h_cons x1 x2) | T_O_54 : forall t1 t2 , O_zr1 t1 -> RCs t1 t2 -> O_zr1 t2 with O_zr2 : St := | T_O_55 : O_zr2 h_0 | T_O_56 : forall t1 t2 , O_zr2 t1 -> RCs t1 t2 -> O_zr2 t2 with O_zr3 : St := | T_O_57 : O_zr3 h_0 | T_O_58 : forall t1 t2 , O_zr3 t1 -> RCs t1 t2 -> O_zr3 t2 with O_zaa : St := | T_O_59 : O_zaa h_nil | T_O_60 : forall x1 x2, O_zr0 x1 -> O_zr1 x2 -> O_zaa (h_cons x1 x2) | T_O_61 : forall x1 x2, O_zr3 x1 -> O_zaa x2 -> O_zaa (h_cons x1 x2) | T_O_62 : forall t1 t2 , O_zaa t1 -> RCs t1 t2 -> O_zaa t2 with O_zab : St := | T_O_63 : forall x1, O_zaa x1 -> O_zab x1 | T_O_64 : forall x1, O_zab x1 -> O_zab (h_tail x1) | T_O_65 : forall t1 t2 , O_zab t1 -> RCs t1 t2 -> O_zab t2 with O_zac : St := | T_O_66 : forall x1, O_zab x1 -> O_zac (h_filter x1) | T_O_67 : forall t1 t2 , O_zac t1 -> RCs t1 t2 -> O_zac t2 with O_zazzzzResult : St := | T_O_68 : forall t1 t2 , O_zazzzzResult t1 -> RCs t1 t2 -> O_zazzzzResult t2 . Scheme Min_O_zr0 := Minimality for O_zr0 Sort Prop with Min_O_zr1 := Minimality for O_zr1 Sort Prop with Min_O_zr2 := Minimality for O_zr2 Sort Prop with Min_O_zr3 := Minimality for O_zr3 Sort Prop with Min_O_zaa := Minimality for O_zaa Sort Prop with Min_O_zab := Minimality for O_zab Sort Prop with Min_O_zac := Minimality for O_zac Sort Prop with Min_O_zazzzzResult := Minimality for O_zazzzzResult Sort Prop . Definition Min_sat_O_zr0 := Min_O_zr0 N_zr0 N_zr1 N_zr2 N_zr2 N_zaa N_zab N_zac N_zazzzzResult . Definition Min_sat_O_zr1 := Min_O_zr1 N_zr0 N_zr1 N_zr2 N_zr2 N_zaa N_zab N_zac N_zazzzzResult . Definition Min_sat_O_zr2 := Min_O_zr2 N_zr0 N_zr1 N_zr2 N_zr2 N_zaa N_zab N_zac N_zazzzzResult . Definition Min_sat_O_zr3 := Min_O_zr3 N_zr0 N_zr1 N_zr2 N_zr2 N_zaa N_zab N_zac N_zazzzzResult . Definition Min_sat_O_zaa := Min_O_zaa N_zr0 N_zr1 N_zr2 N_zr2 N_zaa N_zab N_zac N_zazzzzResult . Definition Min_sat_O_zab := Min_O_zab N_zr0 N_zr1 N_zr2 N_zr2 N_zaa N_zab N_zac N_zazzzzResult . Definition Min_sat_O_zac := Min_O_zac N_zr0 N_zr1 N_zr2 N_zr2 N_zaa N_zab N_zac N_zazzzzResult . Definition Min_sat_O_zazzzzResult := Min_O_zazzzzResult N_zr0 N_zr1 N_zr2 N_zr2 N_zaa N_zab N_zac N_zazzzzResult . (**************************** The correspondent states of O and N. May not be the same state because of the Joins. ****************************) Inductive incl_N : St -> St -> Prop := | Incl_O_zr0 : incl_N O_zr0 N_zr0 | Incl_O_zr1 : incl_N O_zr1 N_zr1 | Incl_O_zr2 : incl_N O_zr2 N_zr2 | Incl_O_zr3 : incl_N O_zr3 N_zr2 | Incl_O_zaa : incl_N O_zaa N_zaa | Incl_O_zab : incl_N O_zab N_zab | Incl_O_zac : incl_N O_zac N_zac | Incl_O_zazzzzResult : incl_N O_zazzzzResult N_zazzzzResult . Ltac empty_zaziInters := match goal with | h : N_zaziInters _ |- _ => inversion h ; fail end . Ltac handle_intcon := match goal with | h2 : ?s2 ?t , h3 : ?s3 ?t |- ?s1 ?t => apply (Automaton_N_satisfies_intersection_constraints s1 s2 s3) ; [ solve [ idtac ] | exact h2 | exact h3 ] end . Ltac handle_rewrite := match goal with | h1 : ?s ?t1 , h2 : RCs ?t1 ?t2 |- ?s ?t2 => apply (Automaton_N_closed_under_RCs s t1 t2) ; [ knownState | exact h1 | exact h2 ] ; fail end . Lemma Automaton_N_is_a_safe_overapproximation_of_automaton_O : forall s_o s_n t, incl_N s_o s_n -> s_o t -> s_n t . Proof. intros s_o s_n t H H0 ; inversion H ; subst ; [ apply Min_sat_O_zr0 | apply Min_sat_O_zr1 | apply Min_sat_O_zr2 | apply Min_sat_O_zr3 | apply Min_sat_O_zaa | apply Min_sat_O_zab | apply Min_sat_O_zac | apply Min_sat_O_zazzzzResult ] ; intros ; solve [ (* the non-intersection-constraint case first *) try empty_zaziInters ; try apply_transitionsN_rec ; (* here we rely on inversionVar to pick the freshest H, i.e. the N one (not the O one) *) inversionVar ; try apply_transitionsN_once | (* intersection constraints *) handle_intcon | (* RCs closure *) handle_rewrite ] . Save. (* User Full Rule Facts (usually, the goal of the analysis) *) Ltac does_not_belong_to_N FR := (* intro negation *) intro ; (* Show (@zzResult !FAIL!) using FR *) cut (N_zazzzzResult h_ziFAILzi) ; [ idtac | apply FR ; assumption ] ; (* Derive a contradiction *) intro Fail_N ; inversion Fail_N . Ltac elim_all_exists_once := match goal with (* exists is Notation for (ex (fun x => _)) *) | h : ex _ |- _ => elim h ; clear h ; intro ; intro end . Ltac elim_all_exists := repeat elim_all_exists_once . Ltac add_useless_hypothesis name := cut True ; [ intro name | trivial ] . Ltac unreachability s_o s_n t incl_s_o h := cut (s_n t) ; [ clear h ; intro ; decomposition | apply (Automaton_N_is_a_safe_overapproximation_of_automaton_O s_o) ; [ apply incl_s_o | assumption ] ] . Ltac cut_on_RCs_snd s := match goal with | h : RCs _ ?t |- _ => cut (s t) end . Lemma FullRule_N_1 : forall x1, N_zac (h_failure x1) -> N_zazzzzResult h_ziFAILzi . Proof. intros ; (apply_transitionsN_once || decomposition) . Save. Lemma Unreachability_1 : ~ exists x1, O_zac (h_failure x1) . Proof. (* Hack: use names x, x0 so that new names start at x1 *) add_useless_hypothesis x ; add_useless_hypothesis x0 ; intro H ; elim_all_exists ; unreachability O_zac N_zac (h_failure x1) Incl_O_zac H . Save.