(****************************
  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.