Require Import Recdef Relations Wellfounded.
Require Import Arith NPeano PeanoNat List Bool Psatz.
Require Import Cecoa.Lib Cecoa.Syntax Cecoa.CBV_cache Cecoa.Bounds Cecoa.Ordering.
Require Import Omega.

Import List.ListNotations.

Section Evaluates.

Variables variable function constructor : Type.

Notation value := (Syntax.value constructor).
Notation term := (Syntax.term variable function constructor).
Notation pattern := (Syntax.pattern variable constructor).
Notation rule := (Syntax.rule variable function constructor).
Notation cbv := (CBV_cache.cbv variable function constructor).
Notation cache := (CBV_cache.cache variable function constructor).

Variable variable_eq_dec : forall (x1 x2 : variable), {x1=x2}+{x1<>x2}.

Variable function_eq_dec : forall (x1 x2 : function), {x1=x2}+{x1<>x2}.

Variable constructor_eq_dec : forall (x1 x2 : constructor), {x1=x2}+{x1<>x2}.

Variable term_default : term.

Variable value_default : value.

Variable function_default : function.

Variable rule_default : rule.

Variable prog : list rule.

Variable max_arity : nat.

Notation wf :=
  (CBV_cache.wf variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity).

Notation assoc_cache := (assoc (term_beq variable_eq_dec function_eq_dec constructor_eq_dec)).

(* Function ranks and compatibility *)

Variable rank: function -> nat.

Hypothesis prog_is_ppo : PPO_prog prog rank.

Hypothesis prog_is_wf : wf_prog max_arity prog.

Definition term_order (t1 t2: term): Prop :=
  In t1 (sub_terms_strict _ _ _ t2).

Set Implicit Arguments.

Lemma term_order_wf : well_founded term_order.
Proof.
(* Goal: @well_founded (Syntax.term variable function constructor) term_order *)
intro t.
induction t as [ x | c lt IH | f lt IH ] using term_ind2;
 constructor; unfold term_order; simpl; [ tauto | | ].

- intros t Hin.
(* Goal: @Acc (Syntax.term variable function constructor) (fun t1 t2 : Syntax.term variable function constructor => @In (Syntax.term variable function constructor) t1 (sub_terms_strict variable function constructor t2)) t *)
  rewrite in_flat_map in Hin.
(* Goal: @Acc (Syntax.term variable function constructor) (fun t1 t2 : Syntax.term variable function constructor => @In (Syntax.term variable function constructor) t1 (sub_terms_strict variable function constructor t2)) t *)
  destruct Hin as (t' & Hin1 & Hin2).
(* Goal: @Acc (Syntax.term variable function constructor) (fun t1 t2 : Syntax.term variable function constructor => @In (Syntax.term variable function constructor) t1 (sub_terms_strict variable function constructor t2)) t *)
  apply sub_term_eq_or_strict in Hin2.
(* Goal: @Acc (Syntax.term variable function constructor) (fun t1 t2 : Syntax.term variable function constructor => @In (Syntax.term variable function constructor) t1 (sub_terms_strict variable function constructor t2)) t *)
  destruct Hin2 as [ Heq | Hin2 ].

  + subst t'.
(* Goal: forall (s s' : list (prod variable (Syntax.value constructor))) (c : constructor) (lv : list (Syntax.value constructor)) (_ : @eq (option (list (prod variable (Syntax.value constructor)))) (unify s (@c_capply constructor c lv) p') (@Some (list (prod variable (Syntax.value constructor))) s')), @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s') p') (@c_capply constructor c lv) *)
     apply IH.
(* Goal: @In (Syntax.term variable function constructor) t' lt *)
     exact Hin1.

  + apply Acc_inv_trans with t'.

    * constructor.
(* Goal: @In (Syntax.term variable function constructor) t (sub_terms_strict variable function constructor t') *)
      exact Hin2.

(* Goal: forall (s s' : list (prod variable (Syntax.value constructor))) (c : constructor) (lv : list (Syntax.value constructor)) (_ : @eq (option (list (prod variable (Syntax.value constructor)))) (unify s (@c_capply constructor c lv) p') (@Some (list (prod variable (Syntax.value constructor))) s')), @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s') p') (@c_capply constructor c lv) *)
    * apply IH.
(* Goal: @In (Syntax.term variable function constructor) t' lt *)
      exact Hin1.

- intros t Hin.
(* Goal: @Acc (Syntax.term variable function constructor) (fun t1 t2 : Syntax.term variable function constructor => @In (Syntax.term variable function constructor) t1 (sub_terms_strict variable function constructor t2)) t *)
  rewrite in_flat_map in Hin.
(* Goal: @Acc (Syntax.term variable function constructor) (fun t1 t2 : Syntax.term variable function constructor => @In (Syntax.term variable function constructor) t1 (sub_terms_strict variable function constructor t2)) t *)
  destruct Hin as (t' & Hin1 & Hin2).
(* Goal: @Acc (Syntax.term variable function constructor) (fun t1 t2 : Syntax.term variable function constructor => @In (Syntax.term variable function constructor) t1 (sub_terms_strict variable function constructor t2)) t *)
  apply sub_term_eq_or_strict in Hin2.
(* Goal: @Acc (Syntax.term variable function constructor) (fun t1 t2 : Syntax.term variable function constructor => @In (Syntax.term variable function constructor) t1 (sub_terms_strict variable function constructor t2)) t *)
  destruct Hin2 as [ Heq | Hin2 ].

  + subst t'.
(* Goal: forall (s s' : list (prod variable (Syntax.value constructor))) (c : constructor) (lv : list (Syntax.value constructor)) (_ : @eq (option (list (prod variable (Syntax.value constructor)))) (unify s (@c_capply constructor c lv) p') (@Some (list (prod variable (Syntax.value constructor))) s')), @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s') p') (@c_capply constructor c lv) *)
     apply IH.
(* Goal: @In (Syntax.term variable function constructor) t' lt *)
     exact Hin1.

  + apply Acc_inv_trans with t'.

    * constructor.
(* Goal: @In (Syntax.term variable function constructor) t (sub_terms_strict variable function constructor t') *)
      exact Hin2.

(* Goal: forall (s s' : list (prod variable (Syntax.value constructor))) (c : constructor) (lv : list (Syntax.value constructor)) (_ : @eq (option (list (prod variable (Syntax.value constructor)))) (unify s (@c_capply constructor c lv) p') (@Some (list (prod variable (Syntax.value constructor))) s')), @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s') p') (@c_capply constructor c lv) *)
    * apply IH.
(* Goal: @In (Syntax.term variable function constructor) t' lt *)
      exact Hin1.
Qed.

Definition active_term := prod function (list value).

Definition term_from_active_term (t: active_term) : term :=
  let (f, lv) := t in
  fapply f (map (@term_from_value _ _ _) lv).

Definition value_list_order (lv lv' : list value) : Prop :=
  suml (map (@value_size _) lv) < suml (map (@value_size _) lv').

Lemma value_list_order_wf : well_founded value_list_order.
Proof.
(* Goal: value_list_order lv lv' *)
unfold value_list_order.
(* Goal: @well_founded (prod function (list (Syntax.value constructor))) (fun t t' : prod function (list (Syntax.value constructor)) => @lexprod nat (list (Syntax.value constructor)) lt value_list_order (@pair nat (list (Syntax.value constructor)) (rank (@fst function (list (Syntax.value constructor)) t)) (@snd function (list (Syntax.value constructor)) t)) (@pair nat (list (Syntax.value constructor)) (rank (@fst function (list (Syntax.value constructor)) t')) (@snd function (list (Syntax.value constructor)) t'))) *)
apply wf_inverse_image.
(* Goal: @well_founded nat lt *)
refine lt_wf.
Defined.

Definition active_term_order_superset t t' :=
  lexprod lt value_list_order (rank (fst t), snd t) (rank (fst t'), snd t').

Definition active_term_order_superset_wf : well_founded active_term_order_superset.
Proof.
(* Goal: active_term_order_superset (@pair function (list (Syntax.value constructor)) f lv) (@pair function (list (Syntax.value constructor)) f' lv') *)
unfold active_term_order_superset.
(* Goal: @well_founded (prod function (list (Syntax.value constructor))) (fun t t' : prod function (list (Syntax.value constructor)) => @lexprod nat (list (Syntax.value constructor)) lt value_list_order (@pair nat (list (Syntax.value constructor)) (rank (@fst function (list (Syntax.value constructor)) t)) (@snd function (list (Syntax.value constructor)) t)) (@pair nat (list (Syntax.value constructor)) (rank (@fst function (list (Syntax.value constructor)) t')) (@snd function (list (Syntax.value constructor)) t'))) *)
apply wf_inverse_image.
(* Goal: @well_founded (prod nat (list (Syntax.value constructor))) (@lexprod nat (list (Syntax.value constructor)) lt value_list_order) *)
apply wf_lexprod.
- apply lt_wf.
- apply value_list_order_wf.
Defined.

Fixpoint unify (s : list (variable * value)) (v : value) (p : pattern) {struct p} :
  option (list (variable * value)) :=
  let unify_list := fix unify_list
    (s : list (variable * value)) (lv : list value) (lp : list pattern) {struct lp} :
    option (list (variable * value)) :=
    match lv, lp with
    | [], [] => Some s
    | v::lv', p::lp' => match unify s v p with
      | None => None
      | Some s' => unify_list s' lv' lp'
      end
    | _, _ => None
    end in
  match p with
  |  p_var x =>
    match assoc (variable_beq variable_eq_dec) x s with
    | None => Some ((x, v) :: s)
    | Some v' => if value_beq constructor_eq_dec v v' then Some s else None
    end
  | p_capply c' lp =>match v with
      | c_capply c lv => if constructor_beq constructor_eq_dec c c' then unify_list s lv lp else None
      end
  end.

Fixpoint unify_list_aux (s : list (variable * value)) (lv : list value) (lp : list pattern) :
  option (list (variable * value)) :=
  match lv, lp with
  | [], [] => Some s
  | v::lv', p::lp' => match unify s v p with
    | None => None
    | Some s' => unify_list_aux s' lv' lp'
    end
  | _, _ => None
  end.

Lemma unify_equation (s : list (variable * value)) (v : value) (p : pattern) :
  unify s v p =
  match p with
  |  p_var x =>
    match assoc (variable_beq variable_eq_dec) x s with
      | None => Some ((x, v) :: s)
      | Some v' => if value_beq constructor_eq_dec v v' then Some s else None
    end
  | p_capply c' lp =>
    match v with
      | c_capply c lv => if constructor_beq constructor_eq_dec c c' then unify_list_aux s lv lp else None
    end
  end.
Proof.
(* Goal: @eq (option (list (prod variable (Syntax.value constructor)))) (unify s v p) match p with | p_var x => match @assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s with | Some v' => if @value_beq constructor constructor_eq_dec v v' then @Some (list (prod variable (Syntax.value constructor))) s else @None (list (prod variable (Syntax.value constructor))) | None => @Some (list (prod variable (Syntax.value constructor))) (@cons (prod variable (Syntax.value constructor)) (@pair variable (Syntax.value constructor) x v) s) end | p_capply c' lp => match v with | c_capply c lv => if @constructor_beq constructor constructor_eq_dec c c' then unify_list_aux s lv lp else @None (list (prod variable (Syntax.value constructor))) end end *)
  revert s v.
  induction p as [ x | c lp IH ] using pattern_ind2;
    [ simpl; trivial | ].
(* Goal: forall (s : list (prod variable (Syntax.value constructor))) (v : Syntax.value constructor), @eq (option (list (prod variable (Syntax.value constructor)))) (unify s v (@p_capply variable constructor c lp)) match v with | c_capply c0 lv => if @constructor_beq constructor constructor_eq_dec c0 c then unify_list_aux s lv lp else @None (list (prod variable (Syntax.value constructor))) end *)
  intros s [ c' lv ].
(* Goal: le (Nat.max (@max_arity_term variable function constructor t) n) (Nat.max (@max_arity_rule variable function constructor (@rule_intro variable function constructor f lp t)) n) *)
  simpl.
(* Goal: @eq (option (list (prod variable (Syntax.value constructor)))) (if @constructor_beq constructor constructor_eq_dec c' c then (fix unify_list (s : list (prod variable (Syntax.value constructor))) (lv : list (Syntax.value constructor)) (lp : list (Syntax.pattern variable constructor)) {struct lp} : option (list (prod variable (Syntax.value constructor))) := match lv with | nil => match lp with | nil => @Some (list (prod variable (Syntax.value constructor))) s | cons p l => @None (list (prod variable (Syntax.value constructor))) end | cons v lv' => match lp with | nil => @None (list (prod variable (Syntax.value constructor))) | cons p lp' => match unify s v p with | Some s' => unify_list s' lv' lp' | None => @None (list (prod variable (Syntax.value constructor))) end end end) s lv lp else @None (list (prod variable (Syntax.value constructor)))) (if @constructor_beq constructor constructor_eq_dec c' c then unify_list_aux s lv lp else @None (list (prod variable (Syntax.value constructor)))) *)
  case constructor_beq; [ | trivial ].
(* Goal: @eq (option (list (prod variable (Syntax.value constructor)))) ((fix unify_list (s : list (prod variable (Syntax.value constructor))) (lv : list (Syntax.value constructor)) (lp : list (Syntax.pattern variable constructor)) {struct lp} : option (list (prod variable (Syntax.value constructor))) := match lv with | nil => match lp with | nil => @Some (list (prod variable (Syntax.value constructor))) s | cons p l => @None (list (prod variable (Syntax.value constructor))) end | cons v lv' => match lp with | nil => @None (list (prod variable (Syntax.value constructor))) | cons p lp' => match unify s v p with | Some s' => unify_list s' lv' lp' | None => @None (list (prod variable (Syntax.value constructor))) end end end) s lv lp) (unify_list_aux s lv lp) *)
  clear c c'; revert s lv.
  induction lp as [ | p lp IHlp ];
    intros s lv;
    [ destruct lv; trivial | ].
(* Goal: @eq (option (list (prod variable (Syntax.value constructor)))) match lv with | nil => @None (list (prod variable (Syntax.value constructor))) | cons v lv' => match unify s v p with | Some s' => (fix unify_list (s : list (prod variable (Syntax.value constructor))) (lv : list (Syntax.value constructor)) (lp : list (Syntax.pattern variable constructor)) {struct lp} : option (list (prod variable (Syntax.value constructor))) := match lv with | nil => match lp with | nil => @Some (list (prod variable (Syntax.value constructor))) s | cons p l => @None (list (prod variable (Syntax.value constructor))) end | cons v0 lv'0 => match lp with | nil => @None (list (prod variable (Syntax.value constructor))) | cons p lp' => match unify s v0 p with | Some s'0 => unify_list s'0 lv'0 lp' | None => @None (list (prod variable (Syntax.value constructor))) end end end) s' lv' lp | None => @None (list (prod variable (Syntax.value constructor))) end end (unify_list_aux s lv (@cons (Syntax.pattern variable constructor) p lp)) *)
  destruct lv as [ | [ c lv' ] lv ]; simpl; trivial.
(* Goal: @eq (option (list (prod variable (Syntax.value constructor)))) match unify s (@c_capply constructor c lv') p with | Some s' => (fix unify_list (s : list (prod variable (Syntax.value constructor))) (lv : list (Syntax.value constructor)) (lp : list (Syntax.pattern variable constructor)) {struct lp} : option (list (prod variable (Syntax.value constructor))) := match lv with | nil => match lp with | nil => @Some (list (prod variable (Syntax.value constructor))) s | cons p l => @None (list (prod variable (Syntax.value constructor))) end | cons v lv' => match lp with | nil => @None (list (prod variable (Syntax.value constructor))) | cons p lp' => match unify s v p with | Some s'0 => unify_list s'0 lv' lp' | None => @None (list (prod variable (Syntax.value constructor))) end end end) s' lv lp | None => @None (list (prod variable (Syntax.value constructor))) end match unify s (@c_capply constructor c lv') p with | Some s' => unify_list_aux s' lv lp | None => @None (list (prod variable (Syntax.value constructor))) end *)
  case unify; trivial.
(* Goal: forall l : list (prod variable (Syntax.value constructor)), @eq (option (list (prod variable (Syntax.value constructor)))) ((fix unify_list (s : list (prod variable (Syntax.value constructor))) (lv : list (Syntax.value constructor)) (lp : list (Syntax.pattern variable constructor)) {struct lp} : option (list (prod variable (Syntax.value constructor))) := match lv with | nil => match lp with | nil => @Some (list (prod variable (Syntax.value constructor))) s | cons p l0 => @None (list (prod variable (Syntax.value constructor))) end | cons v lv' => match lp with | nil => @None (list (prod variable (Syntax.value constructor))) | cons p lp' => match unify s v p with | Some s' => unify_list s' lv' lp' | None => @None (list (prod variable (Syntax.value constructor))) end end end) l lv lp) (unify_list_aux l lv lp) *)
  intros s'.
(* Goal: @eq (option (list (prod variable (Syntax.value constructor)))) ((fix unify_list (s : list (prod variable (Syntax.value constructor))) (lv : list (Syntax.value constructor)) (lp : list (Syntax.pattern variable constructor)) {struct lp} : option (list (prod variable (Syntax.value constructor))) := match lv with | nil => match lp with | nil => @Some (list (prod variable (Syntax.value constructor))) s | cons p l => @None (list (prod variable (Syntax.value constructor))) end | cons v lv' => match lp with | nil => @None (list (prod variable (Syntax.value constructor))) | cons p lp' => match unify s v p with | Some s' => unify_list s' lv' lp' | None => @None (list (prod variable (Syntax.value constructor))) end end end) s' lv lp) (unify_list_aux s' lv lp) *)
  apply IHlp.
(* Goal: forall (p : Syntax.pattern variable constructor) (_ : @In (Syntax.pattern variable constructor) p lp) (s : list (prod variable (Syntax.value constructor))) (v : Syntax.value constructor), @eq (option (list (prod variable (Syntax.value constructor)))) (unify s v p) match p with | p_var x => match @assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s with | Some v' => if @value_beq constructor constructor_eq_dec v v' then @Some (list (prod variable (Syntax.value constructor))) s else @None (list (prod variable (Syntax.value constructor))) | None => @Some (list (prod variable (Syntax.value constructor))) (@cons (prod variable (Syntax.value constructor)) (@pair variable (Syntax.value constructor) x v) s) end | p_capply c' lp => match v with | c_capply c lv => if @constructor_beq constructor constructor_eq_dec c c' then unify_list_aux s lv lp else @None (list (prod variable (Syntax.value constructor))) end end *)
  intros; apply IH; right; assumption.
Qed.

Definition unify_list
  (s : list (variable * value)) (lv : list value) (lp : list pattern) :
  option (variable -> value) :=
  option_map (assoc_default (variable_beq variable_eq_dec) value_default) (unify_list_aux s lv lp).

Lemma unify_list_unify_unify_list :
  forall s s' v lv p lp,
    unify_list_aux s (v :: lv) (p :: lp) = Some s' ->
    exists s'', unify s v p = Some s'' /\ unify_list_aux s'' lv lp = Some s'.
Proof.
(* Goal: forall (s s' : list (prod variable (Syntax.value constructor))) (v : Syntax.value constructor) (lv : list (Syntax.value constructor)) (p : Syntax.pattern variable constructor) (lp : list (Syntax.pattern variable constructor)) (_ : @eq (option (list (prod variable (Syntax.value constructor)))) (unify_list_aux s (@cons (Syntax.value constructor) v lv) (@cons (Syntax.pattern variable constructor) p lp)) (@Some (list (prod variable (Syntax.value constructor))) s')), @ex (list (prod variable (Syntax.value constructor))) (fun s'' : list (prod variable (Syntax.value constructor)) => and (@eq (option (list (prod variable (Syntax.value constructor)))) (unify s v p) (@Some (list (prod variable (Syntax.value constructor))) s'')) (@eq (option (list (prod variable (Syntax.value constructor)))) (unify_list_aux s'' lv lp) (@Some (list (prod variable (Syntax.value constructor))) s'))) *)
  intros s s' v lv p lp.
  case_eq (unify s v p); simpl;
  [ intro s'' | ]; intro Huni; rewrite Huni; [ | discriminate ].
(* Goal: forall _ : @eq (option (list (prod variable (Syntax.value constructor)))) (unify_list_aux s'' lv lp) (@Some (list (prod variable (Syntax.value constructor))) s'), @ex (list (prod variable (Syntax.value constructor))) (fun s''0 : list (prod variable (Syntax.value constructor)) => and (@eq (option (list (prod variable (Syntax.value constructor)))) (@Some (list (prod variable (Syntax.value constructor))) s'') (@Some (list (prod variable (Syntax.value constructor))) s''0)) (@eq (option (list (prod variable (Syntax.value constructor)))) (unify_list_aux s''0 lv lp) (@Some (list (prod variable (Syntax.value constructor))) s'))) *)
  intros Hunis; exists s''.
(* Goal: and (@eq (option (list (prod variable (Syntax.value constructor)))) (@Some (list (prod variable (Syntax.value constructor))) s'') (@Some (list (prod variable (Syntax.value constructor))) s'')) (@eq (option (list (prod variable (Syntax.value constructor)))) (unify_list_aux s'' lv lp) (@Some (list (prod variable (Syntax.value constructor))) s')) *)
  now split.
Qed.

Lemma unify_list_length :
  forall s s' lv lp, unify_list_aux s lv lp = Some s' -> length lv = length lp.
Proof.
  intros s s' lv; revert s s';
  induction lv as [ | v lv IH ]; intros s s' lp Hunis;
  destruct lp; [ trivial | discriminate | discriminate | ].
  simpl; f_equal;
  apply unify_list_unify_unify_list in Hunis;
  destruct Hunis as (s'' & _ & Hunis); now apply IH in Hunis.
Qed.

Lemma unify_cons_eq_unify_list :
  forall s s' c lv c' lp',
    unify s (c_capply c lv) (p_capply c' lp') = Some s' ->
    c = c' /\ unify_list_aux s lv lp' = Some s'.
Proof.
  intros s s' c lv c' lp' Huni;
  rewrite unify_equation in Huni;
  case_eq (constructor_beq constructor_eq_dec c c'); intros Hc; rewrite Hc in Huni;
  [ now rewrite constructor_beq_eq in Hc | discriminate Huni ].
Qed.

Lemma unify_list_aux_extension lv lp s s':
  unify_list_aux s lv lp = Some s' ->
  exists s'',
    s' = s'' ++ s /\
    forall x, assoc (variable_beq variable_eq_dec) x s <> None -> assoc (variable_beq variable_eq_dec) x s'' = None.
Proof.
(* Goal: forall _ : @eq (option (list (prod variable (Syntax.value constructor)))) (unify_list_aux s lv lp) (@Some (list (prod variable (Syntax.value constructor))) s'), @ex (list (prod variable (Syntax.value constructor))) (fun s'' : list (prod variable (Syntax.value constructor)) => and (@eq (list (prod variable (Syntax.value constructor))) s' (@app (prod variable (Syntax.value constructor)) s'' s)) (forall (x : variable) (_ : not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor)))), @eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s'') (@None (Syntax.value constructor)))) *)
  remember (suml (map (value_size (constructor := constructor)) lv)) as size eqn: Hsize.
  revert lv lp s s' Hsize;
    induction size as [ size IH ] using lt_wf_ind; intros lv lp s s' Hsize Hunis.

(* Goal: @ex (list (prod variable (Syntax.value constructor))) (fun s'' : list (prod variable (Syntax.value constructor)) => and (@eq (list (prod variable (Syntax.value constructor))) s' (@app (prod variable (Syntax.value constructor)) s'' s)) (forall (x : variable) (_ : not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor)))), @eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s'') (@None (Syntax.value constructor)))) *)
  destruct lv as [ | v lv ].

  - exists [].
(* Goal: and (@eq (list (prod variable (Syntax.value constructor))) s' (@app (prod variable (Syntax.value constructor)) (@nil (prod variable (Syntax.value constructor))) s)) (forall (x : variable) (_ : not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor)))), @eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x (@nil (prod variable (Syntax.value constructor)))) (@None (Syntax.value constructor))) *)
    assert (Hnil : 0 = length lp) by (now apply unify_list_length in Hunis).
(* Goal: and (@eq (list (prod variable (Syntax.value constructor))) s' (@app (prod variable (Syntax.value constructor)) (@nil (prod variable (Syntax.value constructor))) s)) (forall (x : variable) (_ : not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor)))), @eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x (@nil (prod variable (Syntax.value constructor)))) (@None (Syntax.value constructor))) *)
    destruct lp; [ clear Hnil | now contradict Hnil ].
(* Goal: and (@eq (list (prod variable (Syntax.value constructor))) s' (@app (prod variable (Syntax.value constructor)) (@nil (prod variable (Syntax.value constructor))) s)) (forall (x : variable) (_ : not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor)))), @eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x (@nil (prod variable (Syntax.value constructor)))) (@None (Syntax.value constructor))) *)
    simpl in Hunis; injection Hunis; clear Hunis; intros; now subst s'.

  - assert (Hlen : length (v :: lv) = length lp) by (apply unify_list_length in Hunis; assumption).
(* Goal: @ex (list (prod variable (Syntax.value constructor))) (fun s'' : list (prod variable (Syntax.value constructor)) => and (@eq (list (prod variable (Syntax.value constructor))) s' (@app (prod variable (Syntax.value constructor)) s'' s)) (forall (x : variable) (_ : not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor)))), @eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s'') (@None (Syntax.value constructor)))) *)
    destruct lp as [ | p lp ]; [ discriminate Hlen | clear Hlen ].
(* Goal: @ex (list (prod variable (Syntax.value constructor))) (fun s'' : list (prod variable (Syntax.value constructor)) => and (@eq (list (prod variable (Syntax.value constructor))) s' (@app (prod variable (Syntax.value constructor)) s'' s)) (forall (x : variable) (_ : not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor)))), @eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s'') (@None (Syntax.value constructor)))) *)
    apply unify_list_unify_unify_list in Hunis; destruct Hunis as (s'' & Huni & Hunis).
(* Goal: @ex (list (prod variable (Syntax.value constructor))) (fun s'' : list (prod variable (Syntax.value constructor)) => and (@eq (list (prod variable (Syntax.value constructor))) s' (@app (prod variable (Syntax.value constructor)) s'' s)) (forall (x : variable) (_ : not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor)))), @eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s'') (@None (Syntax.value constructor)))) *)
    set (size' := suml (map (value_size (constructor := constructor)) lv)).
    assert (Hlt: size' < size)
      by (simpl in Hsize; rewrite Hsize;
          change size' with (0 + size'); unfold size';
          apply plus_lt_compat_r;
          destruct v as [ c' lv' ];
          simpl;
          apply lt_O_Sn).
    apply (IH _ Hlt) in Hunis; [ | easy ];
    destruct Hunis as (s''' & Happ & Hconsistent); clear size' Hlt lp.

(* Goal: @ex (list (prod variable (Syntax.value constructor))) (fun s'' : list (prod variable (Syntax.value constructor)) => and (@eq (list (prod variable (Syntax.value constructor))) s' (@app (prod variable (Syntax.value constructor)) s'' s)) (forall (x : variable) (_ : not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor)))), @eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s'') (@None (Syntax.value constructor)))) *)
    destruct p as [ x | c lp' ].

    + simpl in Huni; case_eq (assoc (variable_beq variable_eq_dec) x s).

      * intros v'' Hsome; rewrite Hsome in Huni.
        destruct value_beq in Huni; [ | discriminate Huni ];
        injection Huni; intros; subst s' s''; clear Huni.
(* Goal: @ex (list (prod variable (Syntax.value constructor))) (fun s'' : list (prod variable (Syntax.value constructor)) => and (@eq (list (prod variable (Syntax.value constructor))) (@app (prod variable (Syntax.value constructor)) s''' s) (@app (prod variable (Syntax.value constructor)) s'' s)) (forall (x : variable) (_ : not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor)))), @eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s'') (@None (Syntax.value constructor)))) *)
        now exists s'''.

      * intros Hnone; rewrite Hnone in Huni.
(* Goal: @ex (list (prod variable (Syntax.value constructor))) (fun s'' : list (prod variable (Syntax.value constructor)) => and (@eq (list (prod variable (Syntax.value constructor))) s' (@app (prod variable (Syntax.value constructor)) s'' s)) (forall (x : variable) (_ : not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor)))), @eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s'') (@None (Syntax.value constructor)))) *)
        injection Huni; intro; subst s''; clear Huni.
        exists (s''' ++ [(x,v)]); split; [ now rewrite <- app_assoc | ].
(* Goal: forall (x0 : variable) (_ : not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x0 s) (@None (Syntax.value constructor)))), @eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x0 (@app (prod variable (Syntax.value constructor)) s''' (@cons (prod variable (Syntax.value constructor)) (@pair variable (Syntax.value constructor) x v) (@nil (prod variable (Syntax.value constructor)))))) (@None (Syntax.value constructor)) *)
        intros y Hsome.
(* Goal: forall (x : variable) (_ : @In variable x (@vars_of_term variable function constructor t)), le (@max_arity_term variable function constructor (@term_from_value variable function constructor (s x))) (@max_arity_term variable function constructor t') *)
(* Goal: le (@max_arity_term variable function constructor (@subst variable function constructor s t)) (Nat.max (@max_arity_rule variable function constructor (@rule_intro variable function constructor f lp t)) (@max_arity_term variable function constructor t')) *)
        { rewrite assoc_app_eq_None; split.
          - apply Hconsistent.
            change ((x,v) :: s) with ([(x,v)] ++ s).
(* Goal: not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x (@app (prod variable (Syntax.value constructor)) s''' s'')) (@None (Syntax.value constructor))) *)
            rewrite assoc_app_neq_None; now right.
          - simpl.
(* Goal: @eq (option (Syntax.value constructor)) (if @variable_beq variable variable_eq_dec y x then @Some (Syntax.value constructor) v else @None (Syntax.value constructor)) (@None (Syntax.value constructor)) *)
            case_eq (variable_beq variable_eq_dec y x); [ | easy ].
(* Goal: forall _ : @eq bool (@variable_beq variable variable_eq_dec y x) true, @eq (option (Syntax.value constructor)) (@Some (Syntax.value constructor) v) (@None (Syntax.value constructor)) *)
            rewrite variable_beq_eq; intro; now subst y.
        }

    + destruct v as [ c' lv' ].
(* Goal: @ex (list (prod variable (Syntax.value constructor))) (fun s'' : list (prod variable (Syntax.value constructor)) => and (@eq (list (prod variable (Syntax.value constructor))) s' (@app (prod variable (Syntax.value constructor)) s'' s)) (forall (x : variable) (_ : not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor)))), @eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s'') (@None (Syntax.value constructor)))) *)
      apply unify_cons_eq_unify_list in Huni; destruct Huni as (Hc' & Hunis); subst c'.
(* Goal: @ex (list (prod variable (Syntax.value constructor))) (fun s'' : list (prod variable (Syntax.value constructor)) => and (@eq (list (prod variable (Syntax.value constructor))) s' (@app (prod variable (Syntax.value constructor)) s'' s)) (forall (x : variable) (_ : not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor)))), @eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s'') (@None (Syntax.value constructor)))) *)
      set (size' := suml (map (value_size (constructor := constructor)) lv')).
(* Goal: @ex (list (prod variable (Syntax.value constructor))) (fun s'' : list (prod variable (Syntax.value constructor)) => and (@eq (list (prod variable (Syntax.value constructor))) s' (@app (prod variable (Syntax.value constructor)) s'' s)) (forall (x : variable) (_ : not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor)))), @eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s'') (@None (Syntax.value constructor)))) *)
      assert (Hlt: size' < size) by (subst size; simpl; unfold size'; omega).
      apply (IH _ Hlt) in Hunis; [ | easy ];
      destruct Hunis as (s'''' & Happ' & Hconsistent'); clear size' Hlt.

      exists (s''' ++ s'''').
(* Goal: and (@eq (list (prod variable (Syntax.value constructor))) s' (@app (prod variable (Syntax.value constructor)) (@app (prod variable (Syntax.value constructor)) s''' s'''') s)) (forall (x : variable) (_ : not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor)))), @eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x (@app (prod variable (Syntax.value constructor)) s''' s'''')) (@None (Syntax.value constructor))) *)
      subst s' s''.
      split; [ now rewrite <- app_assoc | ].
(* Goal: forall (x : variable) (_ : not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor)))), @eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x (@app (prod variable (Syntax.value constructor)) s''' s'''')) (@None (Syntax.value constructor)) *)
      intros x Hsome.
(* Goal: @eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x (@app (prod variable (Syntax.value constructor)) s''' s'''')) (@None (Syntax.value constructor)) *)
      rewrite assoc_app_eq_None; split.
      * apply Hconsistent.
(* Goal: not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x (@app (prod variable (Syntax.value constructor)) s'''' s)) (@None (Syntax.value constructor))) *)
        rewrite assoc_app_neq_None; right; assumption.
      * apply Hconsistent'; assumption.
Qed.

Lemma unify_all_vars_defined :
  forall (s s': list (variable * value)) (v: value) (p: pattern),
    unify s v p = Some s' ->
    forall x, In x (vars_of_pattern p) -> assoc (variable_beq variable_eq_dec) x s' <> None.
Proof.
(* Goal: forall (s s' : list (prod variable (Syntax.value constructor))) (v : Syntax.value constructor) (p : Syntax.pattern variable constructor) (_ : @eq (option (list (prod variable (Syntax.value constructor)))) (unify s v p) (@Some (list (prod variable (Syntax.value constructor))) s')) (x : variable) (_ : @In variable x (@vars_of_pattern variable constructor p)), not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s') (@None (Syntax.value constructor))) *)
  intros s s' v p; revert s s' v.
  induction p as [ x | c lp IH ] using pattern_ind2;
    intros s s' v Huni.

  - (* cas variable : unify va forcer s' à contenir x *)
(* Goal: forall (x0 : variable) (_ : @In variable x0 (@vars_of_pattern variable constructor (@p_var variable constructor x))), not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x0 s') (@None (Syntax.value constructor))) *)
    intros x' [ Hx' | H ]; [ | tauto ]; subst x'.
(* Goal: not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s') (@None (Syntax.value constructor))) *)
    rewrite unify_equation in Huni.
(* Goal: @eq (Syntax.value constructor) v' v *)
    case_eq (assoc (variable_beq variable_eq_dec) x s).
    + intros v' Heq; rewrite Heq in Huni.
(* Goal: not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s') (@None (Syntax.value constructor))) *)
      destruct (value_beq _ _ _) in Huni; [ | discriminate ].
(* Goal: not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s') (@None (Syntax.value constructor))) *)
      injection Huni; intros H; subst s'.
(* Goal: not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor))) *)
      rewrite Heq; discriminate.
    + intros Heq; rewrite Heq in Huni; injection Huni; intros H; subst s'.
(* Goal: le (Nat.max (@max_arity_term variable function constructor t) n) (Nat.max (@max_arity_rule variable function constructor (@rule_intro variable function constructor f lp t)) n) *)
      simpl.
(* Goal: not (@eq (option (Syntax.value constructor)) (if @variable_beq variable variable_eq_dec x x then @Some (Syntax.value constructor) v else @assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor))) *)
      case_eq ((variable_beq variable_eq_dec) x x); [ intros; discriminate | ].
      rewrite <- not_true_iff_false, variable_beq_eq; tauto.

  - simpl; destruct v as [ c' lv ].
(* Goal: forall (x : variable) (_ : @In variable x (@flat_map (Syntax.pattern variable constructor) variable (@vars_of_pattern variable constructor) lp)), not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s') (@None (Syntax.value constructor))) *)
    apply unify_cons_eq_unify_list in Huni; destruct Huni as (H & Hunis); subst c'; clear c.
(* Goal: forall (x : variable) (_ : @In variable x (@flat_map (Syntax.pattern variable constructor) variable (@vars_of_pattern variable constructor) lp)), not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s') (@None (Syntax.value constructor))) *)
    revert s s' lv Hunis.
(* Goal: forall (s s' : list (prod variable (Syntax.value constructor))) (lv : list (Syntax.value constructor)) (_ : @eq (option (list (prod variable (Syntax.value constructor)))) (unify_list_aux s lv lp) (@Some (list (prod variable (Syntax.value constructor))) s')) (x : variable) (_ : @In variable x (@flat_map (Syntax.pattern variable constructor) variable (@vars_of_pattern variable constructor) lp)), not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s') (@None (Syntax.value constructor))) *)
    induction lp as [ | p lp IHlp ]; [ easy | ].
    intros s s' [ | v lv ] Hunis;
    [ apply unify_list_length in Hunis; now contradict Hunis | ].
(* Goal: forall (x : variable) (_ : @In variable x (@flat_map (Syntax.pattern variable constructor) variable (@vars_of_pattern variable constructor) (@cons (Syntax.pattern variable constructor) p lp))), not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s') (@None (Syntax.value constructor))) *)
    apply unify_list_unify_unify_list in Hunis.
(* Goal: forall (x : variable) (_ : @In variable x (@flat_map (Syntax.pattern variable constructor) variable (@vars_of_pattern variable constructor) (@cons (Syntax.pattern variable constructor) p lp))), not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s') (@None (Syntax.value constructor))) *)
    destruct Hunis as (s'' & Huni & Hunis).
(* Goal: forall (x : variable) (_ : @In variable x (@flat_map (Syntax.pattern variable constructor) variable (@vars_of_pattern variable constructor) (@cons (Syntax.pattern variable constructor) p lp))), not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s') (@None (Syntax.value constructor))) *)
    intros x; rewrite in_flat_map; intros (p' & [Hp' | Hp'] & Hx).
    + subst p'.
(* Goal: not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s') (@None (Syntax.value constructor))) *)
      apply IH with (x := x) in Huni; [ | now left | easy ].
(* Goal: not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s') (@None (Syntax.value constructor))) *)
      apply unify_list_aux_extension in Hunis.
(* Goal: not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s') (@None (Syntax.value constructor))) *)
      destruct Hunis as (s''' & Heq & _); subst s'.
(* Goal: not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x (@app (prod variable (Syntax.value constructor)) s''' s'')) (@None (Syntax.value constructor))) *)
      rewrite assoc_app_neq_None; now right.
    + apply IHlp with (s := s'') (lv := lv).
      * intros p'' Hin; apply IH; now right.
      * easy.
      * apply in_flat_map.
(* Goal: @ex (Syntax.pattern variable constructor) (fun x0 : Syntax.pattern variable constructor => and (@In (Syntax.pattern variable constructor) x0 lp) (@In variable x (@vars_of_pattern variable constructor x0))) *)
        now exists p'.
Qed.

Lemma eq_psubst_consistent_assoc_extension :
  forall s s' p,
    (forall x, assoc (variable_beq variable_eq_dec) x s <> None -> assoc (variable_beq variable_eq_dec) x s' = None) ->
    (forall x, In x (vars_of_pattern p) -> assoc (variable_beq variable_eq_dec) x s <> None) ->
    psubst (assoc_default (variable_beq variable_eq_dec) value_default (s' ++ s)) p =
    psubst (assoc_default (variable_beq variable_eq_dec) value_default s) p.
Proof.
(* Goal: forall (s s' : list (prod variable (Syntax.value constructor))) (p : Syntax.pattern variable constructor) (_ : forall (x : variable) (_ : not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor)))), @eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s') (@None (Syntax.value constructor))) (_ : forall (x : variable) (_ : @In variable x (@vars_of_pattern variable constructor p)), not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor)))), @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default (@app (prod variable (Syntax.value constructor)) s' s)) p) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s) p) *)
  intros s s' p; revert s s'.
  induction p as [ x | c lp IH ] using pattern_ind2;
    intros s s' Hconsistent Hvars.

  - assert (Hsomes : assoc (variable_beq variable_eq_dec) x s <> None)
      by (apply Hvars; simpl; now left).
    assert (Hnones' : assoc (variable_beq variable_eq_dec) x s' = None)
      by (apply Hconsistent, Hsomes).
    assert (H : exists v, assoc (variable_beq variable_eq_dec) x s = Some v)
      by now apply neq_None_eq_Some.
(* Goal: @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default (@app (prod variable (Syntax.value constructor)) s' s)) (@p_var variable constructor x)) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s) (@p_var variable constructor x)) *)
    clear Hsomes.
(* Goal: @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default (@app (prod variable (Syntax.value constructor)) s' s)) (@p_var variable constructor x)) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s) (@p_var variable constructor x)) *)
    destruct H as (v & Hsome's).
(* Goal: @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default (@app (prod variable (Syntax.value constructor)) s' s)) (@p_var variable constructor x)) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s) (@p_var variable constructor x)) *)
    simpl; unfold assoc_default.
(* Goal: @eq (Syntax.value constructor) match @assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x (@app (prod variable (Syntax.value constructor)) s' s) with | Some b => b | None => value_default end match @assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s with | Some b => b | None => value_default end *)
    rewrite Hsome's.
    case_eq (assoc (variable_beq variable_eq_dec) x (s' ++ s)).
    + intros v'; rewrite assoc_app_eq_Some.
      intros [ Hsomes' | (_ & Hsome) ];
        [ rewrite Hnones' in Hsomes'; discriminate Hsomes'
        | rewrite Hsome's in Hsome; now injection Hsome ].
    + rewrite assoc_app_eq_None; intros (_ & Himpossible); congruence.

  - simpl; f_equal.
(* Goal: @eq (list (Syntax.value constructor)) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default (@app (prod variable (Syntax.value constructor)) s' s))) lp) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s)) lp) *)
    apply map_ext_in.
(* Goal: forall (a : Syntax.pattern variable constructor) (_ : @In (Syntax.pattern variable constructor) a lp), @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default (@app (prod variable (Syntax.value constructor)) s' s)) a) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s) a) *)
    intros p Hin; apply IH; [ assumption | assumption | ].
(* Goal: forall (x : variable) (_ : @In variable x (@vars_of_pattern variable constructor p)), not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor))) *)
    simpl in Hvars.
(* Goal: forall (x : variable) (_ : @In variable x (@vars_of_pattern variable constructor p)), not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor))) *)
    intros x Hx; apply Hvars.
(* Goal: @In variable x (@flat_map (Syntax.pattern variable constructor) variable (@vars_of_pattern variable constructor) lp) *)
    apply in_flat_map; now exists p.
Qed.

Lemma unify_sound :
  forall (s s': list (variable * value)) (v: value) (p: pattern),
    unify s v p = Some s' ->
    psubst (assoc_default (variable_beq variable_eq_dec) value_default s') p = v.
Proof.
(* Goal: forall (s s' : list (prod variable (Syntax.value constructor))) (v : Syntax.value constructor) (p : Syntax.pattern variable constructor) (_ : @eq (option (list (prod variable (Syntax.value constructor)))) (unify s v p) (@Some (list (prod variable (Syntax.value constructor))) s')), @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s') p) v *)
  intros s s' [ c lv ] p; revert s s' c lv.
(* Goal: forall (x : variable) (_ : @In variable x (@vars_of_pattern variable constructor p)), le (@max_arity_term variable function constructor (@term_from_value variable function constructor (s x))) (@max_arity_term variable function constructor (@term_from_value variable function constructor (@psubst variable constructor s p))) *)
  induction p as [ x | c lp IH ] using pattern_ind2.
  - intros s s' c' lv; simpl.
(* Goal: @eq (Syntax.value constructor) v' v *)
    case_eq (assoc (variable_beq variable_eq_dec) x s).
    + intros [ c'' lv'' ] H'' Hassoc.
      case_eq (constructor_beq constructor_eq_dec c' c'');
        case_eq (list_beq value (value_beq constructor_eq_dec) lv lv'');
        intros Heqc Heqlv;
        rewrite Heqc, Heqlv in Hassoc;
        simpl in Hassoc;
        try discriminate.
(* Goal: @eq (Syntax.value constructor) (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s' x) (@c_capply constructor c' lv) *)
      injection Hassoc; intros; subst.
      apply list_beq_eq in Heqc; subst;
      [ | intros; apply value_beq_eq; assumption ].
(* Goal: @eq (Syntax.value constructor) (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s' x) (@c_capply constructor c' lv'') *)
      apply constructor_beq_eq in Heqlv; subst.
(* Goal: @eq (Syntax.value constructor) (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default (@cons (prod variable (Syntax.value constructor)) (@pair variable (Syntax.value constructor) x (@c_capply constructor c' lv)) s) x) (@c_capply constructor c' lv) *)
      unfold assoc_default.
(* Goal: @eq (Syntax.value constructor) match @assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s' with | Some b => b | None => value_default end (@c_capply constructor c'' lv'') *)
      rewrite H''; trivial.
    + intros Hnone Hsome; injection Hsome; intros; subst; clear Hsome.
(* Goal: @eq (Syntax.value constructor) (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default (@cons (prod variable (Syntax.value constructor)) (@pair variable (Syntax.value constructor) x (@c_capply constructor c' lv)) s) x) (@c_capply constructor c' lv) *)
      unfold assoc_default.
(* Goal: le (Nat.max (@max_arity_term variable function constructor t) n) (Nat.max (@max_arity_rule variable function constructor (@rule_intro variable function constructor f lp t)) n) *)
      simpl.
(* Goal: @eq (Syntax.value constructor) match (if @variable_beq variable variable_eq_dec x x then @Some (Syntax.value constructor) (@c_capply constructor c' lv) else @assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) with | Some b => b | None => value_default end (@c_capply constructor c' lv) *)
      case_eq ((variable_beq variable_eq_dec) x x); [ intros; trivial | ].
(* Goal: forall _ : @eq bool (@variable_beq variable variable_eq_dec x x) false, @eq (Syntax.value constructor) match @assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s with | Some b => b | None => value_default end (@c_capply constructor c' lv) *)
      intros Heq.
      rewrite <- not_true_iff_false, variable_beq_eq in Heq.
(* Goal: @eq (Syntax.value constructor) match @assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s with | Some b => b | None => value_default end (@c_capply constructor c' lv) *)
      now contradict Heq.
  - intros s s' c' lv.
(* Goal: forall _ : @eq (option (list (prod variable (Syntax.value constructor)))) (unify s (@c_capply constructor c' lv) (@p_capply variable constructor c lp)) (@Some (list (prod variable (Syntax.value constructor))) s'), @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s') (@p_capply variable constructor c lp)) (@c_capply constructor c' lv) *)
    rewrite unify_equation.
(* Goal: forall _ : @eq (option (list (prod variable (Syntax.value constructor)))) (if @constructor_beq constructor constructor_eq_dec c' c then unify_list_aux s lv lp else @None (list (prod variable (Syntax.value constructor)))) (@Some (list (prod variable (Syntax.value constructor))) s'), @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s') (@p_capply variable constructor c lp)) (@c_capply constructor c' lv) *)
    case_eq (constructor_beq constructor_eq_dec c' c); [ | intros _ H; discriminate H ].
(* Goal: forall (_ : @eq bool (@constructor_beq constructor constructor_eq_dec c' c) true) (_ : @eq (option (list (prod variable (Syntax.value constructor)))) (unify_list_aux s lv lp) (@Some (list (prod variable (Syntax.value constructor))) s')), @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s') (@p_capply variable constructor c lp)) (@c_capply constructor c' lv) *)
    rewrite constructor_beq_eq.
(* Goal: forall (_ : @eq constructor c' c) (_ : @eq (option (list (prod variable (Syntax.value constructor)))) (unify_list_aux s lv lp) (@Some (list (prod variable (Syntax.value constructor))) s')), @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s') (@p_capply variable constructor c lp)) (@c_capply constructor c' lv) *)
    intros Heq; subst.
    revert s s' lv;
    induction lp as [ | p lp IHlp ]; intros s s' lv.
    + destruct lv; [ now simpl | ].
(* Goal: forall _ : @eq (option (list (prod variable (Syntax.value constructor)))) (unify_list_aux s (@cons (Syntax.value constructor) v lv) (@nil (Syntax.pattern variable constructor))) (@Some (list (prod variable (Syntax.value constructor))) s'), @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s') (@p_capply variable constructor c (@nil (Syntax.pattern variable constructor)))) (@c_capply constructor c (@cons (Syntax.value constructor) v lv)) *)
      simpl; intros H; discriminate H.
    + destruct lv as [ | [ c' lv' ] lv ]; [ intros H; discriminate H | ].
(* Goal: le (Nat.max (@max_arity_term variable function constructor t) n) (Nat.max (@max_arity_rule variable function constructor (@rule_intro variable function constructor f lp t)) n) *)
      simpl.
(* Goal: forall _ : @eq (option (list (prod variable (Syntax.value constructor)))) match unify s (@c_capply constructor c' lv') p with | Some s' => unify_list_aux s' lv lp | None => @None (list (prod variable (Syntax.value constructor))) end (@Some (list (prod variable (Syntax.value constructor))) s'), @eq (Syntax.value constructor) (@c_capply constructor c (@cons (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s') p) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s')) lp))) (@c_capply constructor c (@cons (Syntax.value constructor) (@c_capply constructor c' lv') lv)) *)
      case_eq (unify s (c_capply c' lv') p); [ | intros _ H; discriminate H ].
(* Goal: forall (l : list (prod variable (Syntax.value constructor))) (_ : @eq (option (list (prod variable (Syntax.value constructor)))) (unify s (@c_capply constructor c' lv') p) (@Some (list (prod variable (Syntax.value constructor))) l)) (_ : @eq (option (list (prod variable (Syntax.value constructor)))) (unify_list_aux l lv lp) (@Some (list (prod variable (Syntax.value constructor))) s')), @eq (Syntax.value constructor) (@c_capply constructor c (@cons (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s') p) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s')) lp))) (@c_capply constructor c (@cons (Syntax.value constructor) (@c_capply constructor c' lv') lv)) *)
      intros s'' Hs'' Heq.
(* Goal: @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default (@app (prod variable (Syntax.value constructor)) s' s)) (@p_capply variable constructor c lp)) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s) (@p_capply variable constructor c lp)) *)
      f_equal; simpl; f_equal.
(* Goal: @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s') p) (@c_capply constructor c' lv') *)
(* Goal: @eq (list (Syntax.value constructor)) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s')) lp) lv *)
      assert (Hvars' := unify_all_vars_defined _ _ _ Hs'').
(* Goal: @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s') p) (@c_capply constructor c' lv') *)
(* Goal: @eq (list (Syntax.value constructor)) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s')) lp) lv *)
      apply IH in Hs''.
      * apply unify_list_aux_extension in Heq;
        destruct Heq as (s''' & Heq & Hconsistent);
(* Goal: @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s') p) v *)
        subst s'.
(* Goal: @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default (@app (prod variable (Syntax.value constructor)) s''' s'')) p) (@c_capply constructor c' lv') *)
        now rewrite eq_psubst_consistent_assoc_extension.
      * left; trivial.
      * simpl in IHlp.
        assert (Hf_equal : forall lv', c_capply c lv' = c_capply c lv -> lv' = lv)
               by (intros lv'' H''; injection H''; trivial).
(* Goal: @eq (list (Syntax.value constructor)) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s')) lp) lv *)
        apply Hf_equal.
(* Goal: @eq (Syntax.value constructor) (@c_capply constructor c (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s')) lp)) (@c_capply constructor c lv) *)
        apply IHlp with (s := s''); [ | assumption ].
(* Goal: forall (p : Syntax.pattern variable constructor) (_ : @In (Syntax.pattern variable constructor) p lp) (s s' : list (prod variable (Syntax.value constructor))) (c : constructor) (lv : list (Syntax.value constructor)) (_ : @eq (option (list (prod variable (Syntax.value constructor)))) (unify s (@c_capply constructor c lv) p) (@Some (list (prod variable (Syntax.value constructor))) s')), @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s') p) (@c_capply constructor c lv) *)
        intros p' Hin.
(* Goal: forall (s s' : list (prod variable (Syntax.value constructor))) (c : constructor) (lv : list (Syntax.value constructor)) (_ : @eq (option (list (prod variable (Syntax.value constructor)))) (unify s (@c_capply constructor c lv) p') (@Some (list (prod variable (Syntax.value constructor))) s')), @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s') p') (@c_capply constructor c lv) *)
        apply IH.
(* Goal: @In (Syntax.pattern variable constructor) p' (@cons (Syntax.pattern variable constructor) p lp) *)
        right; assumption.
Qed.

Lemma psubst_app p v (s s' : list (variable * value)) :
  (forall x : variable, assoc (variable_beq variable_eq_dec) x s <> None -> assoc (variable_beq variable_eq_dec) x s' = None) ->
  (forall x, In x (vars_of_pattern p) -> assoc (variable_beq variable_eq_dec) x s <> None) ->
  psubst (assoc_default (variable_beq variable_eq_dec) value_default s        ) p = v ->
  psubst (assoc_default (variable_beq variable_eq_dec) value_default (s' ++ s)) p = v.
Proof.
(* Goal: forall (_ : forall (x : variable) (_ : not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor)))), @eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s') (@None (Syntax.value constructor))) (_ : forall (x : variable) (_ : @In variable x (@vars_of_pattern variable constructor p)), not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor)))) (_ : @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s) p) v), @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default (@app (prod variable (Syntax.value constructor)) s' s)) p) v *)
revert v s s'.
(* Goal: forall (v : Syntax.value constructor) (s s' : list (prod variable (Syntax.value constructor))) (_ : forall (x : variable) (_ : not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor)))), @eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s') (@None (Syntax.value constructor))) (_ : forall (x : variable) (_ : @In variable x (@vars_of_pattern variable constructor p)), not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor)))) (_ : @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s) p) v), @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default (@app (prod variable (Syntax.value constructor)) s' s)) p) v *)
induction p as [ x | c lp IHp ] using pattern_ind2; simpl; intros v s s' Hconsistent Hall Hassoc.

- unfold assoc_default in *.
  case_eq (assoc (variable_beq variable_eq_dec) x (s' ++ s)).

  + intros v' Hx.
(* Goal: @eq (Syntax.value constructor) v' v *)
    apply assoc_app_eq_Some in Hx.
(* Goal: @eq (Syntax.value constructor) v' v *)
    destruct Hx as [ Hx | [ Hnone Hx ] ]; [ | rewrite Hx in Hassoc; assumption ].
(* Goal: @eq (Syntax.value constructor) v' v *)
    case_eq (assoc (variable_beq variable_eq_dec) x s).

    * intros v'' Hx'.
(* Goal: @eq (Syntax.value constructor) v' v *)
      rewrite Hx' in Hassoc.
(* Goal: @eq (Syntax.value constructor) v' v *)
      subst v''.
(* Goal: @eq (Syntax.value constructor) v' v *)
      apply eq_None_neq_Some in Hx; [contradict Hx |].
(* Goal: @eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s') (@None (Syntax.value constructor)) *)
      apply Hconsistent.
(* Goal: and (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) P (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) evaluates (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) *)
      auto.

    * intro Hx'.
(* Goal: @eq (Syntax.value constructor) v' v *)
      rewrite Hx' in Hassoc.
(* Goal: @eq (Syntax.value constructor) v' v *)
      apply eq_None_neq_Some in Hx; [contradict Hx |].
(* Goal: @eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s') (@None (Syntax.value constructor)) *)
      apply Hconsistent.
(* Goal: and (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) P (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) evaluates (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) *)
      auto.

  + intro Hassoc'.
(* Goal: @eq (Syntax.value constructor) value_default v *)
    apply assoc_app_eq_None in Hassoc'.
(* Goal: @eq (Syntax.value constructor) value_default v *)
    destruct Hassoc' as [_ Hassoc'].
(* Goal: @eq (Syntax.value constructor) value_default v *)
    rewrite Hassoc' in Hassoc.
(* Goal: @eq (Syntax.value constructor) value_default v *)
    assumption.

- rewrite <- Hassoc.
(* Goal: @eq nat (@value_size constructor v) (@value_size constructor v') *)
  f_equal.
(* Goal: @eq (list (Syntax.value constructor)) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default (@app (prod variable (Syntax.value constructor)) s' s))) lp) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s)) lp) *)
  apply map_in_ext.
(* Goal: forall (a : Syntax.pattern variable constructor) (_ : @In (Syntax.pattern variable constructor) a lp), @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default (@app (prod variable (Syntax.value constructor)) s' s)) a) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s) a) *)
  intros p Hp.
(* Goal: @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default (@app (prod variable (Syntax.value constructor)) s' s)) p) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s) p) *)
  apply eq_psubst_consistent_assoc_extension; [ assumption | ].
(* Goal: forall (x : variable) (_ : @In variable x (@vars_of_pattern variable constructor p)), not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s'') (@None (Syntax.value constructor))) *)
  intros x Hx.
(* Goal: not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s) (@None (Syntax.value constructor))) *)
  apply Hall.
(* Goal: @In (Syntax.term variable function constructor) t1 (@flat_map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (sub_terms variable function constructor) l) *)
  apply in_flat_map.
(* Goal: and (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) P (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) evaluates (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) *)
  eauto.
Qed.

Lemma unify_list_sound :
  forall (lp : list pattern) (lv : list value) (s : variable -> value),
    unify_list [] lv lp = Some s -> map (psubst s) lp = lv.
Proof.
assert (
  Hgen: forall lv lp s0 s, unify_list s0 lv lp = Some s ->
  map (psubst s) lp = lv
).
(* Goal: forall (x : variable) (_ : @In variable x (@vars_of_term variable function constructor t)), le (@max_arity_term variable function constructor (@term_from_value variable function constructor (s x))) (@max_arity_term variable function constructor t') *)
(* Goal: le (@max_arity_term variable function constructor (@subst variable function constructor s t)) (Nat.max (@max_arity_rule variable function constructor (@rule_intro variable function constructor f lp t)) (@max_arity_term variable function constructor t')) *)
{
(* Goal: forall (lv : list (Syntax.value constructor)) (lp : list (Syntax.pattern variable constructor)) (s0 : list (prod variable (Syntax.value constructor))) (s : forall _ : variable, Syntax.value constructor) (_ : @eq (option (forall _ : variable, Syntax.value constructor)) (unify_list s0 lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)), @eq (list (Syntax.value constructor)) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp) lv *)
unfold unify_list.
induction lv as [ | v lv IHlv ]; intros [ | p lp ] s0 s Hula;
 [ trivial | simpl in Hula; discriminate Hula | simpl in Hula; discriminate Hula | ].
(* Goal: @eq (list (Syntax.value constructor)) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) (@cons (Syntax.pattern variable constructor) p lp)) (@cons (Syntax.value constructor) v lv) *)
unfold option_map in Hula.
case_eq (unify_list_aux s0 (v :: lv) (p :: lp));
 [ | intro Hnone; rewrite Hnone in Hula; discriminate Hula ].
(* Goal: forall (v : forall _ : variable, Syntax.value constructor) (_ : @eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp0) (@Some (forall _ : variable, Syntax.value constructor) v)) (_ : @eq (option (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor))) (@Some (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) (@pair (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor) (@pair nat (forall _ : variable, Syntax.value constructor) O v) (@subst variable function constructor v t0))) (@Some (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) (@pair (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor) (@pair nat (forall _ : variable, Syntax.value constructor) i s) t))), @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt i (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) match i with | O => @rule_intro variable function constructor f0 lp0 t0 | S m => @nth (Syntax.rule variable function constructor) m prog' rule_default end (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
intros s' Hs'.
(* Goal: @eq (list (Syntax.value constructor)) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) (@cons (Syntax.pattern variable constructor) p lp)) (@cons (Syntax.value constructor) v lv) *)
rewrite Hs' in Hula.
(* Goal: @eq (list (Syntax.value constructor)) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) (@cons (Syntax.pattern variable constructor) p lp)) (@cons (Syntax.value constructor) v lv) *)
injection Hula; clear Hula; intro; subst s.
(* Goal: @eq (list (Syntax.value constructor)) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s')) (@cons (Syntax.pattern variable constructor) p lp)) (@cons (Syntax.value constructor) v lv) *)
apply unify_list_unify_unify_list in Hs'.
(* Goal: @eq (list (Syntax.value constructor)) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s')) (@cons (Syntax.pattern variable constructor) p lp)) (@cons (Syntax.value constructor) v lv) *)
destruct Hs' as (s'' & Hs'' & Hs').
(* Goal: le (Nat.max (@max_arity_term variable function constructor t) n) (Nat.max (@max_arity_rule variable function constructor (@rule_intro variable function constructor f lp t)) n) *)
simpl.
(* Goal: @eq nat (@value_size constructor v) (@value_size constructor v') *)
f_equal.

- assert(HHs'' := Hs'').
(* Goal: @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s') p) v *)
  apply unify_sound in Hs''.
(* Goal: @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s') p) v *)
  assert(HHs' := Hs').
(* Goal: @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s') p) v *)
  apply unify_list_aux_extension in Hs'.
(* Goal: @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s') p) v *)
  destruct Hs' as (s''' & Hs' & Hconsistent).
(* Goal: @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s') p) v *)
  subst s'.
(* Goal: @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default (@app (prod variable (Syntax.value constructor)) s''' s'')) p) v *)
  apply psubst_app; [ assumption | | assumption ].
(* Goal: forall (x : variable) (_ : @In variable x (@vars_of_pattern variable constructor p)), not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s'') (@None (Syntax.value constructor))) *)
  intros x Hx.
(* Goal: not (@eq (option (Syntax.value constructor)) (@assoc variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) x s'') (@None (Syntax.value constructor))) *)
  eapply unify_all_vars_defined; [ exact HHs'' | exact Hx].

- eapply IHlv with (s0 := s'').
(* Goal: @eq (option (forall _ : variable, Syntax.value constructor)) (@option_map (list (prod variable (Syntax.value constructor))) (forall _ : variable, Syntax.value constructor) (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default) (unify_list_aux s'' lv lp)) (@Some (forall _ : variable, Syntax.value constructor) (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s')) *)
  rewrite Hs'.
(* Goal: @eq (option (forall _ : variable, Syntax.value constructor)) (@option_map (list (prod variable (Syntax.value constructor))) (forall _ : variable, Syntax.value constructor) (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default) (@Some (list (prod variable (Syntax.value constructor))) s')) (@Some (forall _ : variable, Syntax.value constructor) (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s')) *)
  reflexivity.
}
(* Goal: and (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) P (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) evaluates (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) *)
eauto.
Qed.

Fixpoint first_rule_rec (prog': list rule) (t: active_term) :
  option (nat * (variable -> value) * term) :=
  match prog' with
    | [] => None
  | rule_intro f lp t' :: prog'' =>
    if function_beq function_eq_dec (fst t) f
    then
      match unify_list [] (snd t) lp with
        | None =>
          match first_rule_rec prog'' t with
            | None => None
            | Some (i, s, t) => Some (S i, s, t)
            end
        | Some s => Some (0, s, subst s t')
      end
    else
      match first_rule_rec prog'' t with
        | None => None
        | Some (i, s, t) => Some (S i, s, t)
      end
  end.

Definition first_rule (t: active_term) :
  option (nat * (variable -> value) * term) :=
  first_rule_rec prog t.

Global Arguments first_rule t : simpl never.

Lemma first_rule_sound :
  forall (f: function) (lv: list value) (i: nat) (s: variable -> value) (t: term),
  first_rule (f, lv) = Some (i, s, t) ->
  { lpt : (list pattern * term)| let (lp, t') := lpt in
    i < length prog /\
    nth i prog rule_default = rule_intro f lp t' /\
    unify_list [] lv lp = Some s /\
    t = subst s t'}.
Proof.
(* Goal: forall (f : function) (lv : list (Syntax.value constructor)) (i : nat) (s : forall _ : variable, Syntax.value constructor) (t : Syntax.term variable function constructor) (_ : @eq (option (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor))) (first_rule (@pair function (list (Syntax.value constructor)) f lv)) (@Some (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) (@pair (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor) (@pair nat (forall _ : variable, Syntax.value constructor) i s) t))), @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt i (@length (Syntax.rule variable function constructor) prog)) (and (@eq (Syntax.rule variable function constructor) (@nth (Syntax.rule variable function constructor) i prog rule_default) (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
  clear prog_is_ppo prog_is_wf.
(* Goal: forall (f : function) (lv : list (Syntax.value constructor)) (i : nat) (s : forall _ : variable, Syntax.value constructor) (t : Syntax.term variable function constructor) (_ : @eq (option (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor))) (first_rule (@pair function (list (Syntax.value constructor)) f lv)) (@Some (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) (@pair (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor) (@pair nat (forall _ : variable, Syntax.value constructor) i s) t))), @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt i (@length (Syntax.rule variable function constructor) prog)) (and (@eq (Syntax.rule variable function constructor) (@nth (Syntax.rule variable function constructor) i prog rule_default) (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
  unfold first_rule.
  induction prog as [ | r0 prog' IHp ];
    simpl; intros f lv i s t; [ intros H; discriminate H | ].
(* Goal: forall _ : @eq (option (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor))) match r0 with | rule_intro f0 lp t' => if @function_beq function function_eq_dec f f0 then match unify_list (@nil (prod variable (Syntax.value constructor))) lv lp with | Some s => @Some (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) (@pair (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor) (@pair nat (forall _ : variable, Syntax.value constructor) O s) (@subst variable function constructor s t')) | None => match first_rule_rec prog' (@pair function (list (Syntax.value constructor)) f lv) with | Some (pair (pair i s as p0) t as p) => @Some (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) (@pair (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor) (@pair nat (forall _ : variable, Syntax.value constructor) (S i) s) t) | None => @None (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) end end else match first_rule_rec prog' (@pair function (list (Syntax.value constructor)) f lv) with | Some (pair (pair i s as p0) t as p) => @Some (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) (@pair (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor) (@pair nat (forall _ : variable, Syntax.value constructor) (S i) s) t) | None => @None (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) end end (@Some (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) (@pair (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor) (@pair nat (forall _ : variable, Syntax.value constructor) i s) t)), @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt i (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) match i with | O => r0 | S m => @nth (Syntax.rule variable function constructor) m prog' rule_default end (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
  destruct r0 as [ f0 lp0 t0 ].
(* Goal: forall _ : @eq (option (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor))) (if @function_beq function function_eq_dec f f0 then match unify_list (@nil (prod variable (Syntax.value constructor))) lv lp0 with | Some s => @Some (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) (@pair (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor) (@pair nat (forall _ : variable, Syntax.value constructor) O s) (@subst variable function constructor s t0)) | None => match first_rule_rec prog' (@pair function (list (Syntax.value constructor)) f lv) with | Some (pair (pair i s as p0) t as p) => @Some (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) (@pair (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor) (@pair nat (forall _ : variable, Syntax.value constructor) (S i) s) t) | None => @None (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) end end else match first_rule_rec prog' (@pair function (list (Syntax.value constructor)) f lv) with | Some (pair (pair i s as p0) t as p) => @Some (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) (@pair (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor) (@pair nat (forall _ : variable, Syntax.value constructor) (S i) s) t) | None => @None (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) end) (@Some (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) (@pair (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor) (@pair nat (forall _ : variable, Syntax.value constructor) i s) t)), @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt i (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) match i with | O => @rule_intro variable function constructor f0 lp0 t0 | S m => @nth (Syntax.rule variable function constructor) m prog' rule_default end (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
  case_eq (function_beq function_eq_dec f f0).
  - intro Heqf; rewrite function_beq_eq in Heqf.
(* Goal: forall _ : @eq (option (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor))) match unify_list (@nil (prod variable (Syntax.value constructor))) lv lp0 with | Some s => @Some (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) (@pair (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor) (@pair nat (forall _ : variable, Syntax.value constructor) O s) (@subst variable function constructor s t0)) | None => match first_rule_rec prog' (@pair function (list (Syntax.value constructor)) f lv) with | Some (pair (pair i s as p0) t as p) => @Some (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) (@pair (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor) (@pair nat (forall _ : variable, Syntax.value constructor) (S i) s) t) | None => @None (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) end end (@Some (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) (@pair (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor) (@pair nat (forall _ : variable, Syntax.value constructor) i s) t)), @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt i (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) match i with | O => @rule_intro variable function constructor f0 lp0 t0 | S m => @nth (Syntax.rule variable function constructor) m prog' rule_default end (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
    case_eq (unify_list [] lv lp0).
    + intros s' Hs'.
(* Goal: forall _ : @eq (option (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor))) (@Some (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) (@pair (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor) (@pair nat (forall _ : variable, Syntax.value constructor) O s') (@subst variable function constructor s' t0))) (@Some (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) (@pair (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor) (@pair nat (forall _ : variable, Syntax.value constructor) i s) t)), @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt i (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) match i with | O => @rule_intro variable function constructor f0 lp0 t0 | S m => @nth (Syntax.rule variable function constructor) m prog' rule_default end (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
      intros H; injection H; clear H.
(* Goal: forall (_ : @eq (Syntax.term variable function constructor) (@subst variable function constructor s' t0) t) (_ : @eq (forall _ : variable, Syntax.value constructor) s' s) (_ : @eq nat O i), @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt i (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) match i with | O => @rule_intro variable function constructor f0 lp0 t0 | S m => @nth (Syntax.rule variable function constructor) m prog' rule_default end (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
      intros Heqt Heqs Hi.
(* Goal: @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt i (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) match i with | O => @rule_intro variable function constructor f0 lp0 t0 | S m => @nth (Syntax.rule variable function constructor) m prog' rule_default end (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
      subst s' t f0 i.
(* Goal: @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt O (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) (@rule_intro variable function constructor f lp0 t0) (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) (@subst variable function constructor s t0) (@subst variable function constructor s t'))))) *)
      exists (lp0, t0).
(* Goal: and (lt O (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) (@rule_intro variable function constructor f lp0 t0) (@rule_intro variable function constructor f lp0 t0)) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp0) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) (@subst variable function constructor s t0) (@subst variable function constructor s t0)))) *)
      repeat split; [ apply lt_O_Sn | assumption ].
    + (* ici on dispose d’une hypothèse unify_list = None *)
(* Goal: forall (_ : @eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp0) (@None (forall _ : variable, Syntax.value constructor))) (_ : @eq (option (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor))) match first_rule_rec prog' (@pair function (list (Syntax.value constructor)) f lv) with | Some (pair (pair i s as p0) t as p) => @Some (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) (@pair (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor) (@pair nat (forall _ : variable, Syntax.value constructor) (S i) s) t) | None => @None (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) end (@Some (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) (@pair (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor) (@pair nat (forall _ : variable, Syntax.value constructor) i s) t))), @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt i (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) match i with | O => @rule_intro variable function constructor f0 lp0 t0 | S m => @nth (Syntax.rule variable function constructor) m prog' rule_default end (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
      intros Hnone Hrec.
(* Goal: @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt i (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) match i with | O => @rule_intro variable function constructor f0 lp0 t0 | S m => @nth (Syntax.rule variable function constructor) m prog' rule_default end (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
      case_eq (first_rule_rec prog' (f,lv)); [ | intros H; rewrite H in Hrec; discriminate Hrec ].
(* Goal: forall (p : prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) (_ : @eq (option (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor))) (first_rule_rec prog' (@pair function (list (Syntax.value constructor)) f lv)) (@Some (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) p)), @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt i (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) match i with | O => @rule_intro variable function constructor f0 lp0 t0 | S m => @nth (Syntax.rule variable function constructor) m prog' rule_default end (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
      intros [ [i' s'] t'] Heq.
(* Goal: @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt i (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) match i with | O => @rule_intro variable function constructor f0 lp0 t0 | S m => @nth (Syntax.rule variable function constructor) m prog' rule_default end (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
      rewrite Heq in Hrec.
(* Goal: @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt i (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) match i with | O => @rule_intro variable function constructor f0 lp0 t0 | S m => @nth (Syntax.rule variable function constructor) m prog' rule_default end (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
      injection Hrec; clear Hrec; intros; subst.
(* Goal: @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt (S i') (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) (@nth (Syntax.rule variable function constructor) i' prog' rule_default) (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
      apply IHp in Heq.
(* Goal: @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt (S i') (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) (@nth (Syntax.rule variable function constructor) i' prog' rule_default) (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
      destruct Heq as [[lp t'] Hlpt].
(* Goal: @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt (S i') (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) (@nth (Syntax.rule variable function constructor) i' prog' rule_default) (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
      exists (lp, t').
(* Goal: and (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) P (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) evaluates (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) *)
      repeat split; try tauto.
(* Goal: lt (S i') (S (@length (Syntax.rule variable function constructor) prog')) *)
      omega.

  - intros Hneq Hrec.
(* Goal: @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt i (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) match i with | O => @rule_intro variable function constructor f0 lp0 t0 | S m => @nth (Syntax.rule variable function constructor) m prog' rule_default end (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
    case_eq (first_rule_rec prog' (f,lv)); [ | intros H; rewrite H in Hrec; discriminate Hrec ].
(* Goal: forall (p : prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) (_ : @eq (option (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor))) (first_rule_rec prog' (@pair function (list (Syntax.value constructor)) f lv)) (@Some (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) p)), @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt i (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) match i with | O => @rule_intro variable function constructor f0 lp0 t0 | S m => @nth (Syntax.rule variable function constructor) m prog' rule_default end (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
    intros [ [i' s'] t'] Heq.
(* Goal: @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt i (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) match i with | O => @rule_intro variable function constructor f0 lp0 t0 | S m => @nth (Syntax.rule variable function constructor) m prog' rule_default end (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
    rewrite Heq in Hrec.
(* Goal: @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt i (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) match i with | O => @rule_intro variable function constructor f0 lp0 t0 | S m => @nth (Syntax.rule variable function constructor) m prog' rule_default end (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
    injection Hrec; clear Hrec; intros; subst.
(* Goal: @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt (S i') (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) (@nth (Syntax.rule variable function constructor) i' prog' rule_default) (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
    apply IHp in Heq.
(* Goal: @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt (S i') (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) (@nth (Syntax.rule variable function constructor) i' prog' rule_default) (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
    destruct Heq as [[lp t'] Hlpt].
(* Goal: @sig (prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor)) (fun lpt : prod (list (Syntax.pattern variable constructor)) (Syntax.term variable function constructor) => let (lp, t') := lpt in and (lt (S i') (S (@length (Syntax.rule variable function constructor) prog'))) (and (@eq (Syntax.rule variable function constructor) (@nth (Syntax.rule variable function constructor) i' prog' rule_default) (@rule_intro variable function constructor f lp t')) (and (@eq (option (forall _ : variable, Syntax.value constructor)) (unify_list (@nil (prod variable (Syntax.value constructor))) lv lp) (@Some (forall _ : variable, Syntax.value constructor) s)) (@eq (Syntax.term variable function constructor) t (@subst variable function constructor s t'))))) *)
    exists (lp, t').
(* Goal: and (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) P (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) evaluates (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) *)
    repeat split; try tauto.
(* Goal: lt (S i') (S (@length (Syntax.rule variable function constructor) prog')) *)
    omega.
Qed.

Definition active_term_order_superset_dec: forall (t t': active_term), {active_term_order_superset t t'} + {~ active_term_order_superset t t'}.
Proof.
(* Goal: forall t t' : active_term, sumbool (active_term_order_superset t t') (not (active_term_order_superset t t')) *)
intros t t'.
(* Goal: sumbool (active_term_order_superset t t') (not (active_term_order_superset t t')) *)
apply lex_prod_dec.
- apply eq_nat_dec.

- apply lt_dec.

- intros x y.
(* Goal: value_list_order lv lv' *)
  unfold value_list_order.
(* Goal: sumbool (lt (suml (@map (Syntax.value constructor) nat (@value_size constructor) x)) (suml (@map (Syntax.value constructor) nat (@value_size constructor) y))) (not (lt (suml (@map (Syntax.value constructor) nat (@value_size constructor) x)) (suml (@map (Syntax.value constructor) nat (@value_size constructor) y)))) *)
  apply lt_dec.
Defined.

Definition lex : (active_term * term) -> (active_term * term) -> Prop :=
  lexprod active_term_order_superset term_order.

Lemma wf_lex : well_founded lex.
Proof.
(* Goal: @well_founded (prod active_term (Syntax.term variable function constructor)) lex *)
exact (wf_lexprod active_term_order_superset_wf term_order_wf).
Qed.

Lemma sub_terms_trans t1 t2 t3:
  In t1 (sub_terms variable function constructor t2) ->
  In t2 (sub_terms _ _ _ t3) ->
  In t1 (sub_terms _ _ _ t3).
Proof.
induction t3 using term_ind2; intros H1 H2; simpl in *.
- destruct H2 as [Heq | Hf].
  + subst t2.
(* Goal: or (@eq (Syntax.term variable function constructor) (@var variable function constructor x) t1) False *)
    left; now inversion H1.

  + inversion Hf.

- destruct H2 as [Heq |Hin].
  + subst t2.
(* Goal: or (@eq (Syntax.term variable function constructor) (@fapply variable function constructor f l) t1) (@In (Syntax.term variable function constructor) t1 (@flat_map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (sub_terms variable function constructor) l)) *)
    exact H1.

  + right.
    rewrite in_flat_map in *.
(* Goal: @ex (Syntax.term variable function constructor) (fun x : Syntax.term variable function constructor => and (@In (Syntax.term variable function constructor) x l) (@In (Syntax.term variable function constructor) t1 (sub_terms variable function constructor x))) *)
    destruct Hin as (x & Hin & Hx).
(* Goal: @ex (Syntax.term variable function constructor) (fun x : Syntax.term variable function constructor => and (@In (Syntax.term variable function constructor) x l) (@In (Syntax.term variable function constructor) t1 (sub_terms variable function constructor x))) *)
    exists x.
(* Goal: and (@In (Syntax.term variable function constructor) x l) (@In (Syntax.term variable function constructor) t1 (sub_terms variable function constructor x)) *)
    split; [exact Hin |].
(* Goal: and (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) P (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) evaluates (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) *)
    auto.

- destruct H2 as [Heq |Hin].
  + subst t2.
(* Goal: or (@eq (Syntax.term variable function constructor) (@fapply variable function constructor f l) t1) (@In (Syntax.term variable function constructor) t1 (@flat_map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (sub_terms variable function constructor) l)) *)
    exact H1.

  + right.
    rewrite in_flat_map in *.
(* Goal: @ex (Syntax.term variable function constructor) (fun x : Syntax.term variable function constructor => and (@In (Syntax.term variable function constructor) x l) (@In (Syntax.term variable function constructor) t1 (sub_terms variable function constructor x))) *)
    destruct Hin as (x & Hin & Hx).
(* Goal: @ex (Syntax.term variable function constructor) (fun x : Syntax.term variable function constructor => and (@In (Syntax.term variable function constructor) x l) (@In (Syntax.term variable function constructor) t1 (sub_terms variable function constructor x))) *)
    exists x.
(* Goal: and (@In (Syntax.term variable function constructor) x l) (@In (Syntax.term variable function constructor) t1 (sub_terms variable function constructor x)) *)
    split; [exact Hin |].
(* Goal: and (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) P (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) evaluates (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) *)
    auto.
Qed.

Lemma sub_terms_strict_trans t1 t2 t3:
  In t1 (sub_terms_strict variable function constructor t2) ->
  In t2 (sub_terms_strict _ _ _ t3) ->
  In t1 (sub_terms_strict _ _ _ t3).
Proof.
(* Goal: forall (_ : forall (b : A) (_ : R b a) (l' : list A) (_ : @W A R l'), @W A R (@cons A b l')) (_ : @W A R l), @W A R (@cons A a l) *)
intros H1 H2.
(* Goal: @In (Syntax.term variable function constructor) t1 (sub_terms_strict variable function constructor t3) *)
destruct t3.
- inversion H2.

- simpl in *.
(* Goal: @In (Syntax.term variable function constructor) t1 (@flat_map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (sub_terms variable function constructor) l) *)
  apply in_flat_map in H2.
(* Goal: @In (Syntax.term variable function constructor) t1 (@flat_map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (sub_terms variable function constructor) l) *)
  apply sub_term_strict_incl in H1.
(* Goal: @In (Syntax.term variable function constructor) t1 (@flat_map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (sub_terms variable function constructor) l) *)
  destruct H2 as (x & Hin & Hx).
(* Goal: @In (Syntax.term variable function constructor) t1 (@flat_map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (sub_terms variable function constructor) l) *)
  apply in_flat_map.
(* Goal: @ex (Syntax.term variable function constructor) (fun x : Syntax.term variable function constructor => and (@In (Syntax.term variable function constructor) x l) (@In (Syntax.term variable function constructor) t1 (sub_terms variable function constructor x))) *)
  exists x; split; [exact Hin | now apply sub_terms_trans with t2].

- simpl in *.
(* Goal: @In (Syntax.term variable function constructor) t1 (@flat_map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (sub_terms variable function constructor) l) *)
  apply in_flat_map in H2.
(* Goal: @In (Syntax.term variable function constructor) t1 (@flat_map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (sub_terms variable function constructor) l) *)
  apply sub_term_strict_incl in H1.
(* Goal: @In (Syntax.term variable function constructor) t1 (@flat_map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (sub_terms variable function constructor) l) *)
  destruct H2 as (x & Hin & Hx).
(* Goal: @In (Syntax.term variable function constructor) t1 (@flat_map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (sub_terms variable function constructor) l) *)
  apply in_flat_map.
(* Goal: @ex (Syntax.term variable function constructor) (fun x : Syntax.term variable function constructor => and (@In (Syntax.term variable function constructor) x l) (@In (Syntax.term variable function constructor) t1 (sub_terms variable function constructor x))) *)
  exists x; split; [exact Hin | now apply sub_terms_trans with t2].
Qed.

Lemma lex_trans a1 a2 a3:
  lex a1 a2 -> lex a2 a3 -> lex a1 a3.
Proof.
(* Goal: forall (_ : forall (b : A) (_ : R b a) (l' : list A) (_ : @W A R l'), @W A R (@cons A b l')) (_ : @W A R l), @W A R (@cons A a l) *)
intros H1 H2.
(* Goal: lex a1 a3 *)
refine (lexprod_trans _ _ H1 H2).
- intros x1 x2 x3 Hx1 Hx2. 
(* Goal: active_term_order_superset x1 x3 *)
  refine (lexprod_trans lt_trans _ Hx1 Hx2).
(* Goal: forall (b1 b2 b3 : list (Syntax.value constructor)) (_ : value_list_order b1 b2) (_ : value_list_order b2 b3), value_list_order b1 b3 *)
  intros v1 v2 v3 Hv1 Hv2.
(* Goal: value_list_order v1 v3 *)
  eapply lt_trans; [exact Hv1 | exact Hv2].
- intros.
(* Goal: and (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) P (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) evaluates (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) *)
  eapply sub_terms_strict_trans; eauto.
Qed.



Inductive list_order {A : Type} (R : A -> A -> Prop) : list A -> list A -> Prop :=
| lo_cons:  forall l1 l2 h, Forall (fun x => R x h) l1 -> list_order R (l1 ++ l2) (h :: l2).

Definition W {A : Type} (R : A -> A -> Prop) (l : list A) : Prop :=
  Acc (list_order R) l.
(*  forall l', list_order R l' l -> Acc (list_order R) l'. *)

Lemma deuxpointun (A : Type) (R : A -> A -> Prop) (l : list A) (a : A) :
  (forall b, R b a -> forall l', W R l' -> W R (b :: l')) ->
   W R l (* /\
   (forall l', list_order R l' l -> W R (a :: l')) *) ->
  W R (a :: l).
Proof.
(* Goal: forall (_ : forall (b : A) (_ : R b a) (l' : list A) (_ : @W A R l'), @W A R (@cons A b l')) (_ : @W A R l), @W A R (@cons A a l) *)
  intros H1 H2.
(* Goal: @W A R (@cons A a l) *)
  constructor; intros l' Hlo.
(* Goal: @Acc (list A) (@list_order A R) l' *)
  inversion Hlo; subst.
(* Goal: @Acc (list A) (@list_order A R) (@app A l1 l) *)
  induction l1.
  - simpl in *.
(* Goal: evaluates (@term_from_value variable function constructor (@c_capply constructor c l)) (@c_capply constructor c l) *)
    constructor.
(* Goal: forall (y : list A) (_ : @list_order A R y l), @Acc (list A) (@list_order A R) y *)
    apply H2.

  - constructor.
(* Goal: forall (y : list A) (_ : @list_order A R y (@app A (@cons A a0 l1) l)), @Acc (list A) (@list_order A R) y *)
    assert (Ha0 : R a0 a) by (inversion H3; assumption).
(* Goal: forall (y : list A) (_ : @list_order A R y (@app A (@cons A a0 l1) l)), @Acc (list A) (@list_order A R) y *)
    apply (H1 a0 Ha0).
(* Goal: @W A R ((fix app (l m : list A) {struct l} : list A := match l with | nil => m | cons a l1 => @cons A a (app l1 m) end) l1 l) *)
    unfold W.
(* Goal: @eq (Syntax.value constructor) value_default v *)
    apply IHl1; try constructor; inversion H3; assumption.
Qed.

Lemma deuxpointdeux (A : Type) (R : A -> A -> Prop) (l : list A) (a : A) : 
  (forall b, R b a -> forall l, W R l -> W R (b :: l)) ->
  (forall l, W R l -> W R (a :: l)).
Proof.
(* Goal: forall (_ : forall (b : A) (_ : R b a) (l : list A) (_ : @W A R l), @W A R (@cons A b l)) (l : list A) (_ : @W A R l), @W A R (@cons A a l) *)
intros H l' Hacc.
(* Goal: @W A R (@cons A a l') *)
induction Hacc as [l'' Hl'' _].
(* Goal: @W A R (@cons A a l'') *)
apply deuxpointun.
- intros b Hb l' Hl'.
(* Goal: @W A R (@cons A b l') *)
  now apply H.

- now constructor.
Qed.

Lemma deuxpointtrois (A : Type) (R : A -> A -> Prop) (l : list A) (a : A) :
  well_founded R -> W R l -> W R (a :: l).
Proof.
(* Goal: forall (_ : @well_founded A R) (_ : @W A R l), @W A R (@cons A a l) *)
intros HR.
(* Goal: forall (_ : lt n (@length A l)) (_ : @eq A (@nth A n l d) x), @In A x l *)
revert l.
(* Goal: forall (l : list A) (_ : @W A R l), @W A R (@cons A a l) *)
induction (HR a).
(* Goal: forall (l : list A) (_ : @W A R l), @W A R (@cons A x l) *)
intros l Hl.
(* Goal: @W A R (@cons A x l) *)
eapply deuxpointdeux; [ exact l | | exact Hl ].
(* Goal: forall (b : A) (_ : R b x) (l : list A) (_ : @W A R l), @W A R (@cons A b l) *)
intros b Hb l' Hl'.
(* Goal: @W A R (@cons A b l') *)
now apply H0.
Qed.

Lemma list_order_wf (A : Type) (R : A -> A -> Prop) :
  well_founded R -> well_founded (list_order R).
Proof.
(* Goal: forall _ : @well_founded A R, @well_founded (list A) (@list_order A R) *)
intro HwfR.
(* Goal: @well_founded (list A) (@list_order A R) *)
intro l.
(* Goal: @Acc (list A) (@list_order A R) l *)
induction l.
- constructor.
(* Goal: forall (_ : evaluates t v) (_ : le (@max_arity_term variable function constructor t) max_arity), @ex (CBV_cache.cbv variable function constructor) (fun p : CBV_cache.cbv variable function constructor => and (@CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p) (and (@eq (Syntax.value constructor) (@proj_right variable function constructor p) v) (@eq (Syntax.term variable function constructor) (@proj_left variable function constructor p) t))) *)
  intros.
(* Goal: @Acc (list A) (@list_order A R) y *)
  inversion H.

- now apply deuxpointtrois.
Qed.

Lemma product_suml_lt l1 l2 : 
  product lt l1 l2 ->
  suml l1 < suml l2.
Proof.
(* Goal: forall _ : @product nat lt l1 l2, lt (suml l1) (suml l2) *)
intro Hprod.
(* Goal: lt (suml l1) (suml l2) *)
induction Hprod.
- simpl; subst; omega.

- simpl.
(* Goal: lt (Init.Nat.add x (suml xs)) (Init.Nat.add y (suml ys)) *)
  apply plus_lt_le_compat; [assumption|].
(* Goal: le (suml xs) (suml ys) *)
  induction H0.
  + trivial.

  + assert (x0 <= y0) by (destruct H0; omega).
(* Goal: lt (S i') (S (@length (Syntax.rule variable function constructor) prog')) *)
     simpl; omega.
Qed.

Lemma PPO_active_term_order_superset act act' :
  PPO rank (term_from_active_term act) (term_from_active_term act') ->
  active_term_order_superset act act'.
Proof.
(* Goal: forall _ : @PPO variable function constructor rank (term_from_active_term act) (term_from_active_term act'), active_term_order_superset act act' *)
intro HPPO.
(* Goal: active_term_order_superset act act' *)
destruct act as (f & lv).
(* Goal: active_term_order_superset (@pair function (list (Syntax.value constructor)) f lv) act' *)
destruct act' as (f' & lv').
(* Goal: active_term_order_superset (@pair function (list (Syntax.value constructor)) f lv) (@pair function (list (Syntax.value constructor)) f' lv') *)
simpl in HPPO.
(* Goal: active_term_order_superset (@pair function (list (Syntax.value constructor)) f lv) (@pair function (list (Syntax.value constructor)) f' lv') *)
inversion HPPO; subst.
- apply in_map_iff in H1.
(* Goal: active_term_order_superset (@pair function (list (Syntax.value constructor)) f lv) (@pair function (list (Syntax.value constructor)) f' lv') *)
  destruct H1 as (v & Hv & _).
(* Goal: active_term_order_superset (@pair function (list (Syntax.value constructor)) f lv) (@pair function (list (Syntax.value constructor)) f' lv') *)
  destruct v.
(* Goal: active_term_order_superset (@pair function (list (Syntax.value constructor)) f lv) (@pair function (list (Syntax.value constructor)) f' lv') *)
  inversion Hv.

- apply in_map_iff in H2.
(* Goal: active_term_order_superset (@pair function (list (Syntax.value constructor)) f lv) (@pair function (list (Syntax.value constructor)) f' lv') *)
  destruct H2 as (v & Hv & _).
(* Goal: active_term_order_superset (@pair function (list (Syntax.value constructor)) f lv) (@pair function (list (Syntax.value constructor)) f' lv') *)
  subst t.
(* Goal: active_term_order_superset (@pair function (list (Syntax.value constructor)) f lv) (@pair function (list (Syntax.value constructor)) f' lv') *)
  contradict H3.
(* Goal: le (suml (@nil nat)) (suml (@nil nat)) *)
  apply fapply_not_PPO_value; trivial.
(* Goal: and (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) P (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) evaluates (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) *)
  apply term_value_eqv; eauto.

- now left.

- unfold active_term_order_superset.
(* Goal: le (Nat.max (@max_arity_term variable function constructor t) n) (Nat.max (@max_arity_rule variable function constructor (@rule_intro variable function constructor f lp t)) n) *)
  simpl.
(* Goal: @lexprod nat (list (Syntax.value constructor)) lt value_list_order (@pair nat (list (Syntax.value constructor)) (rank f) lv) (@pair nat (list (Syntax.value constructor)) (rank f') lv') *)
  rewrite H2.
(* Goal: @clos_refl nat lt (@value_size constructor v) (@value_size constructor v') *)
  right.
(* Goal: value_list_order lv lv' *)
  unfold value_list_order.
(* Goal: lt (suml (@map (Syntax.value constructor) nat (@value_size constructor) lv)) (suml (@map (Syntax.value constructor) nat (@value_size constructor) lv')) *)
  apply product_suml_lt.
(* Goal: @product nat lt (@map (Syntax.value constructor) nat (@value_size constructor) lv) (@map (Syntax.value constructor) nat (@value_size constructor) lv') *)
  clear f f' H2 HPPO.
(* Goal: @product nat lt (@map (Syntax.value constructor) nat (@value_size constructor) lv) (@map (Syntax.value constructor) nat (@value_size constructor) lv') *)
  revert H4; intros Hppo.
(* Goal: @product nat lt (@map (Syntax.value constructor) nat (@value_size constructor) lv) (@map (Syntax.value constructor) nat (@value_size constructor) lv') *)
  assert (Hlen := Hppo).
(* Goal: @product nat lt (@map (Syntax.value constructor) nat (@value_size constructor) lv) (@map (Syntax.value constructor) nat (@value_size constructor) lv') *)
  apply product_length in Hlen.
(* Goal: @product nat lt (@map (Syntax.value constructor) nat (@value_size constructor) lv) (@map (Syntax.value constructor) nat (@value_size constructor) lv') *)
  do 2 rewrite map_length in Hlen.
  revert lv' Hppo Hlen;
    induction lv as [ | v lv IH ];
    intros lv' Hppo Hlen;
    destruct lv' as [ | v' lv' ];
    simpl in *;
    try discriminate Hlen.

  + inversion Hppo.

  + revert Hppo;
    set (lt := map (@term_from_value _ _ _) lv : list term);
    set (lt' := map (@term_from_value _ _ _) lv' : list term);
    intros Hppo.
(* Goal: @Forall2 nat nat (@clos_refl nat lt) (@cons nat (@value_size constructor v) (@map (Syntax.value constructor) nat (@value_size constructor) lv)) (@cons nat (@value_size constructor v') (@map (Syntax.value constructor) nat (@value_size constructor) lv')) *)
    apply eq_add_S in Hlen.
(* Goal: @product nat lt (@cons nat (@value_size constructor v) (@map (Syntax.value constructor) nat (@value_size constructor) lv)) (@cons nat (@value_size constructor v') (@map (Syntax.value constructor) nat (@value_size constructor) lv')) *)
    inversion Hppo; subst.

    * apply term_from_value_injective in H2; subst v'.
(* Goal: le (suml (@nil nat)) (suml (@nil nat)) *)
      apply product_conseq; trivial.
(* Goal: @eq (Syntax.value constructor) value_default v *)
      apply IH; assumption.

    * apply product_consst;
      [ apply (PPO_value_lt_size variable function) with (rank := rank); assumption | ].

(* Goal: forall (x : variable) (_ : @In variable x (@vars_of_term variable function constructor t)), le (@max_arity_term variable function constructor (@term_from_value variable function constructor (s x))) (@max_arity_term variable function constructor t') *)
(* Goal: le (@max_arity_term variable function constructor (@subst variable function constructor s t)) (Nat.max (@max_arity_rule variable function constructor (@rule_intro variable function constructor f lp t)) (@max_arity_term variable function constructor t')) *)
      { clear Hppo v v' IH H2;
        revert lt lv' lt' Hlen H4;
        induction lv as [ | v lv IH ];
        intros lt lv' lt' Hlen Hfor;
        destruct lv' as [ | v' lv' ];
        [ constructor
        | inversion Hlen
        | inversion Hlen
        | ].

(* Goal: @Forall2 nat nat (@clos_refl nat Peano.lt) (@map (Syntax.value constructor) nat (@value_size constructor) (@cons (Syntax.value constructor) v lv)) (@map (Syntax.value constructor) nat (@value_size constructor) (@cons (Syntax.value constructor) v' lv')) *)
        subst lt lt'.
        simpl in *.
(* Goal: @Forall2 nat nat (@clos_refl nat lt) (@cons nat (@value_size constructor v) (@map (Syntax.value constructor) nat (@value_size constructor) lv)) (@cons nat (@value_size constructor v') (@map (Syntax.value constructor) nat (@value_size constructor) lv')) *)
        apply eq_add_S in Hlen.
(* Goal: evaluates (@term_from_value variable function constructor (@c_capply constructor c l)) (@c_capply constructor c l) *)
        constructor.

        - inversion Hfor; subst.
(* Goal: @clos_refl nat lt (@value_size constructor v) (@value_size constructor v') *)
          destruct H2.
          + left.
(* Goal: @eq (Syntax.value constructor) value_default v *)
            apply (PPO_value_lt_size variable function) with (rank := rank); assumption.
          + right.
(* Goal: @eq nat (@value_size constructor v) (@value_size constructor v') *)
            f_equal.
(* Goal: @eq (Syntax.value constructor) value_default v *)
            apply (@term_from_value_injective variable function); assumption.
        - apply IH;
          [ | inversion Hfor ];
(* Goal: @eq (Syntax.value constructor) value_default v *)
          assumption.
      }
Qed.

Lemma term_order_PPO t1 t2 : term_order t1 t2 -> PPO rank t1 t2.
Proof.
(* Goal: forall _ : term_order t1 t2, @PPO variable function constructor rank t1 t2 *)
intro Horder.
(* Goal: @PPO variable function constructor rank t1 t2 *)
unfold term_order in Horder.
(* Goal: @PPO variable function constructor rank t1 t2 *)
induction t2 using term_ind2.
- inversion Horder.

- simpl in Horder.
(* Goal: @PPO variable function constructor rank t1 (@fapply variable function constructor f l) *)
  apply in_flat_map in Horder.
(* Goal: @PPO variable function constructor rank t1 (@fapply variable function constructor f l) *)
  destruct Horder as (t' & Hin & Ht').
(* Goal: @PPO variable function constructor rank t1 (@fapply variable function constructor f l) *)
  apply PPO_trans_eq with t'.
  + apply sub_term_eq_or_strict in Ht'.
(* Goal: @clos_refl (Syntax.term variable function constructor) (@PPO variable function constructor rank) t1 t' *)
    destruct Ht' as [Heq | Ht'].
    * now subst; right.

    * left; apply H; assumption.

  + now apply ppo_constr_in.

- simpl in Horder.
(* Goal: @PPO variable function constructor rank t1 (@fapply variable function constructor f l) *)
  apply in_flat_map in Horder.
(* Goal: @PPO variable function constructor rank t1 (@fapply variable function constructor f l) *)
  destruct Horder as (t' & Hin & Ht').
(* Goal: @PPO variable function constructor rank t1 (@fapply variable function constructor f l) *)
  apply PPO_trans_eq with t'.
  + apply sub_term_eq_or_strict in Ht'.
(* Goal: @clos_refl (Syntax.term variable function constructor) (@PPO variable function constructor rank) t1 t' *)
    destruct Ht' as [Heq | Ht'].
    * now subst; right.

    * left; apply H; assumption.

  + now apply ppo_fun_in.
Qed.

Lemma max_arity_subst s t f lp :
  rule_vars_defined (rule_intro f lp t) ->
  let t' := fapply f (map (fun p => term_from_value variable function (@psubst variable constructor s p)) lp) in
  max_arity_term (subst s t) <= Nat.max (max_arity_rule (rule_intro f lp t)) (max_arity_term t').
Proof.
(* Goal: forall _ : @rule_vars_defined variable function constructor (@rule_intro variable function constructor f lp t), let t' := @fapply variable function constructor f (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (fun p : Syntax.pattern variable constructor => @term_from_value variable function constructor (@psubst variable constructor s p)) lp) in le (@max_arity_term variable function constructor (@subst variable function constructor s t)) (Nat.max (@max_arity_rule variable function constructor (@rule_intro variable function constructor f lp t)) (@max_arity_term variable function constructor t')) *)
  intros Hvars t'.
  assert (Hn : forall x, In x (vars_of_term t) ->
                   max_arity_term (term_from_value variable function (s x)) <= max_arity_term t').
(* Goal: forall (x : variable) (_ : @In variable x (@vars_of_term variable function constructor t)), le (@max_arity_term variable function constructor (@term_from_value variable function constructor (s x))) (@max_arity_term variable function constructor t') *)
  { subst t'.
(* Goal: le (Nat.max (@max_arity_term variable function constructor t) n) (Nat.max (@max_arity_rule variable function constructor (@rule_intro variable function constructor f lp t)) n) *)
    intros x Hx; apply Hvars in Hx; simpl.
(* Goal: @clos_refl nat lt (@value_size constructor v) (@value_size constructor v') *)
    rewrite PeanoNat.Nat.max_le_iff; right.
(* Goal: le (@max_arity_term variable function constructor (@term_from_value variable function constructor (s x))) (maxl (@map (Syntax.term variable function constructor) nat (@max_arity_term variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (fun p : Syntax.pattern variable constructor => @term_from_value variable function constructor (@psubst variable constructor s p)) lp))) *)
    clear t f Hvars.
(* Goal: le (@max_arity_term variable function constructor (@term_from_value variable function constructor (s x))) (maxl (@map (Syntax.term variable function constructor) nat (@max_arity_term variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (fun p : Syntax.pattern variable constructor => @term_from_value variable function constructor (@psubst variable constructor s p)) lp))) *)
    rewrite in_flat_map in Hx; destruct Hx as (p & Hp & Hvars).
(* Goal: le (@max_arity_term variable function constructor (@term_from_value variable function constructor (s x))) (@max_arity_term variable function constructor (@term_from_value variable function constructor (@psubst variable constructor s (@p_capply variable constructor c lp)))) *)
    transitivity (max_arity_term (term_from_value variable function (psubst s p))).
    - clear lp Hp; revert x Hvars.
(* Goal: forall (x : variable) (_ : @In variable x (@vars_of_pattern variable constructor p)), le (@max_arity_term variable function constructor (@term_from_value variable function constructor (s x))) (@max_arity_term variable function constructor (@term_from_value variable function constructor (@psubst variable constructor s p))) *)
      induction p as [ x | c lp IH ] using pattern_ind2.
      + simpl.
(* Goal: @eq (option (list (prod variable (Syntax.value constructor)))) (unify_list_aux s'' lv lp) (@Some (list (prod variable (Syntax.value constructor))) s') *)
        intros x' H; destruct H; [ subst x' | ]; easy.
      + intros x Hx; simpl in Hx.
(* Goal: le (@max_arity_term variable function constructor (@term_from_value variable function constructor (s x))) (@max_arity_term variable function constructor (@term_from_value variable function constructor (@psubst variable constructor s (@p_capply variable constructor c lp)))) *)
        apply in_flat_map in Hx; destruct Hx as (p & Hp & Hvars).
(* Goal: le (@max_arity_term variable function constructor (@term_from_value variable function constructor (s x))) (@max_arity_term variable function constructor (@term_from_value variable function constructor (@psubst variable constructor s (@p_capply variable constructor c lp)))) *)
        transitivity (max_arity_term (term_from_value variable function (psubst s p))).
(* Goal: forall (s s' : list (prod variable (Syntax.value constructor))) (c : constructor) (lv : list (Syntax.value constructor)) (_ : @eq (option (list (prod variable (Syntax.value constructor)))) (unify s (@c_capply constructor c lv) p') (@Some (list (prod variable (Syntax.value constructor))) s')), @eq (Syntax.value constructor) (@psubst variable constructor (@assoc_default variable (Syntax.value constructor) (@variable_beq variable variable_eq_dec) value_default s') p') (@c_capply constructor c lv) *)
        * now apply IH.
        * simpl.
(* Goal: @clos_refl nat lt (@value_size constructor v) (@value_size constructor v') *)
          rewrite PeanoNat.Nat.max_le_iff; right.
(* Goal: le (@max_arity_term variable function constructor (@term_from_value variable function constructor (@psubst variable constructor s p))) (maxl (@map (Syntax.term variable function constructor) nat (@max_arity_term variable function constructor) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp)))) *)
          now apply maxl_is_max, in_map, in_map, in_map.
    - apply maxl_is_max, in_map.
      set (t := term_from_value _ _ _);
      change (term_from_value _ _ _) with ((fun p => term_from_value variable function (psubst s p)) p) in t;
(* Goal: active_term_order_superset (@pair function (list (Syntax.value constructor)) f lv) (@pair function (list (Syntax.value constructor)) f' lv') *)
        subst t.
(* Goal: @In (Syntax.term variable function constructor) ((fun p : Syntax.pattern variable constructor => @term_from_value variable function constructor (@psubst variable constructor s p)) p) (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (fun p : Syntax.pattern variable constructor => @term_from_value variable function constructor (@psubst variable constructor s p)) lp) *)
      now apply in_map.
  }

(* Goal: le (@max_arity_term variable function constructor (@subst variable function constructor s t)) (Nat.max (@max_arity_rule variable function constructor (@rule_intro variable function constructor f lp t)) (@max_arity_term variable function constructor t')) *)
  remember (max_arity_term t') as n eqn: Heq; clear Heq.
(* Goal: le (@max_arity_term variable function constructor (@subst variable function constructor s t)) (Nat.max (@max_arity_rule variable function constructor (@rule_intro variable function constructor f lp t)) n) *)
  transitivity (Nat.max (max_arity_term t) n).
  - clear f lp t' Hvars.
(* Goal: le (@max_arity_term variable function constructor (@subst variable function constructor s t)) (Nat.max (@max_arity_term variable function constructor t) n) *)
    induction t as [ x | c lt IH | f lt IH ] using term_ind2.
    + simpl; apply Hn.
(* Goal: active_term_order_superset (@pair function (list (Syntax.value constructor)) f lv) (@pair function (list (Syntax.value constructor)) f' lv') *)
      simpl; now left.

    + simpl; rewrite <- Max.max_assoc.
(* Goal: le (Nat.max (@length (Syntax.term variable function constructor) (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (@subst variable function constructor s) lt)) (maxl (@map (Syntax.term variable function constructor) nat (@max_arity_term variable function constructor) (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (@subst variable function constructor s) lt)))) (Nat.max (@length (Syntax.term variable function constructor) lt) (Nat.max (maxl (@map (Syntax.term variable function constructor) nat (@max_arity_term variable function constructor) lt)) n)) *)
      apply Nat.max_le_compat; [ now rewrite map_length | ].
(* Goal: le (maxl (@map (Syntax.term variable function constructor) nat (@max_arity_term variable function constructor) (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (@subst variable function constructor s) lt))) (Nat.max (maxl (@map (Syntax.term variable function constructor) nat (@max_arity_term variable function constructor) lt)) n) *)
      simpl in Hn; clear c.
(* Goal: le (maxl (@map (Syntax.term variable function constructor) nat (@max_arity_term variable function constructor) (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (@subst variable function constructor s) lt))) (Nat.max (maxl (@map (Syntax.term variable function constructor) nat (@max_arity_term variable function constructor) lt)) n) *)
      induction lt as [ | t lt IHlt ]; [ now apply le_O_n | ].
(* Goal: le (Nat.max (@max_arity_term variable function constructor t) n) (Nat.max (@max_arity_rule variable function constructor (@rule_intro variable function constructor f lp t)) n) *)
      simpl.
(* Goal: le (Nat.max (@max_arity_term variable function constructor (@subst variable function constructor s t)) (maxl (@map (Syntax.term variable function constructor) nat (@max_arity_term variable function constructor) (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (@subst variable function constructor s) lt)))) (Nat.max (Nat.max (@max_arity_term variable function constructor t) (maxl (@map (Syntax.term variable function constructor) nat (@max_arity_term variable function constructor) lt))) n) *)
      set (ml := maxl _) at 2.
      replace (Nat.max (Nat.max (max_arity_term t) ml) n)
      with (Nat.max (Nat.max (max_arity_term t) n) (Nat.max ml n));
        [ | now rewrite <- Max.max_assoc, (Max.max_assoc n), (Max.max_comm n),
            <- (Max.max_assoc ml), Max.max_idempotent, Max.max_assoc ].
(* Goal: le (Nat.max (@max_arity_term variable function constructor (@subst variable function constructor s t)) (maxl (@map (Syntax.term variable function constructor) nat (@max_arity_term variable function constructor) (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (@subst variable function constructor s) lt)))) (Nat.max (Nat.max (@max_arity_term variable function constructor t) n) (Nat.max ml n)) *)
      subst ml; apply Nat.max_le_compat.

      * apply IH; [ now left | ].
(* Goal: forall (x : variable) (_ : @In variable x (@vars_of_term variable function constructor t)), le (@max_arity_term variable function constructor (@term_from_value variable function constructor (s x))) n *)
        intros x Hx; apply Hn.
(* Goal: @clos_refl nat lt (@value_size constructor v) (@value_size constructor v') *)
        now simpl; apply in_or_app; left.

      * apply IHlt.
(* Goal: @clos_refl nat lt (@value_size constructor v) (@value_size constructor v') *)
        now intros t' Ht'; apply IH; right.
(* Goal: @clos_refl nat lt (@value_size constructor v) (@value_size constructor v') *)
        now intros x Hx; apply Hn; simpl; apply in_or_app; right.

    + simpl; rewrite <- Max.max_assoc.
(* Goal: le (Nat.max (@length (Syntax.term variable function constructor) (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (@subst variable function constructor s) lt)) (maxl (@map (Syntax.term variable function constructor) nat (@max_arity_term variable function constructor) (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (@subst variable function constructor s) lt)))) (Nat.max (@length (Syntax.term variable function constructor) lt) (Nat.max (maxl (@map (Syntax.term variable function constructor) nat (@max_arity_term variable function constructor) lt)) n)) *)
      apply Nat.max_le_compat; [ now rewrite map_length | ].
(* Goal: le (maxl (@map (Syntax.term variable function constructor) nat (@max_arity_term variable function constructor) (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (@subst variable function constructor s) lt))) (Nat.max (maxl (@map (Syntax.term variable function constructor) nat (@max_arity_term variable function constructor) lt)) n) *)
      simpl in Hn; clear f.
(* Goal: le (maxl (@map (Syntax.term variable function constructor) nat (@max_arity_term variable function constructor) (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (@subst variable function constructor s) lt))) (Nat.max (maxl (@map (Syntax.term variable function constructor) nat (@max_arity_term variable function constructor) lt)) n) *)
      induction lt as [ | t lt IHlt ]; [ now apply le_O_n | ].
(* Goal: le (Nat.max (@max_arity_term variable function constructor t) n) (Nat.max (@max_arity_rule variable function constructor (@rule_intro variable function constructor f lp t)) n) *)
      simpl.
(* Goal: le (Nat.max (@max_arity_term variable function constructor (@subst variable function constructor s t)) (maxl (@map (Syntax.term variable function constructor) nat (@max_arity_term variable function constructor) (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (@subst variable function constructor s) lt)))) (Nat.max (Nat.max (@max_arity_term variable function constructor t) (maxl (@map (Syntax.term variable function constructor) nat (@max_arity_term variable function constructor) lt))) n) *)
      set (ml := maxl _) at 2.
      replace (Nat.max (Nat.max (max_arity_term t) ml) n)
      with (Nat.max (Nat.max (max_arity_term t) n) (Nat.max ml n));
        [ | now rewrite <- Max.max_assoc, (Max.max_assoc n), (Max.max_comm n),
            <- (Max.max_assoc ml), Max.max_idempotent, Max.max_assoc ].
(* Goal: le (Nat.max (@max_arity_term variable function constructor (@subst variable function constructor s t)) (maxl (@map (Syntax.term variable function constructor) nat (@max_arity_term variable function constructor) (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (@subst variable function constructor s) lt)))) (Nat.max (Nat.max (@max_arity_term variable function constructor t) n) (Nat.max ml n)) *)
      subst ml; apply Nat.max_le_compat.

      * apply IH; [ now left | ].
(* Goal: forall (x : variable) (_ : @In variable x (@vars_of_term variable function constructor t)), le (@max_arity_term variable function constructor (@term_from_value variable function constructor (s x))) n *)
        intros x Hx; apply Hn.
(* Goal: @clos_refl nat lt (@value_size constructor v) (@value_size constructor v') *)
        now simpl; apply in_or_app; left.

      * apply IHlt.
(* Goal: @clos_refl nat lt (@value_size constructor v) (@value_size constructor v') *)
        now intros t' Ht'; apply IH; right.
(* Goal: @clos_refl nat lt (@value_size constructor v) (@value_size constructor v') *)
        now intros x Hx; apply Hn; simpl; apply in_or_app; right.

  - simpl.
(* Goal: le (Nat.max (@max_arity_term variable function constructor t) n) (Nat.max (Nat.max (@max_arity_term variable function constructor t) (Nat.max (@length (Syntax.pattern variable constructor) lp) (maxl (@map (Syntax.pattern variable constructor) nat (@max_arity_pattern variable constructor) lp)))) n) *)
    apply PeanoNat.Nat.max_le_compat_r.
(* Goal: le (@max_arity_term variable function constructor t) (Nat.max (@max_arity_term variable function constructor t) (Nat.max (@length (Syntax.pattern variable constructor) lp) (maxl (@map (Syntax.pattern variable constructor) nat (@max_arity_pattern variable constructor) lp)))) *)
    now apply PeanoNat.Nat.le_max_l.
Qed.

Lemma first_rule_max_arity act t i s :
  wf_prog max_arity prog ->
  first_rule act = Some (i, s, t) ->
  max_arity_term (term_from_active_term act) <= max_arity ->
  max_arity_term t <= max_arity.
Proof.
intros Hwfprog Hrule.
destruct act as [f lv].
apply first_rule_sound in Hrule.
destruct Hrule as ([lp'  t''] & Hlengthi & Heqi & Hunify_list & Hsubst).
(* Goal: active_term_order_superset (@pair function (list (Syntax.value constructor)) f lv) (@pair function (list (Syntax.value constructor)) f' lv') *)
subst t.
etransitivity.
- apply max_arity_subst with (f := f) (lp := lp').
  eapply andl_in; [ apply Hwfprog | ].
  apply in_map.
  rewrite <- Heqi.
  now apply nth_In.
- apply Max.max_lub.
   + etransitivity; [ apply maxl_is_max  | apply Hwfprog].
       apply in_map.
       rewrite <- Heqi.
(* Goal: le (suml (@nil nat)) (suml (@nil nat)) *)
       apply nth_In; trivial.
   + rewrite <- map_map.
(* Goal: and (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) P (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) evaluates (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) *)
      erewrite unify_list_sound; eauto.
Qed.



Inductive evaluates : term -> value -> Prop :=
| CAPPLY : forall lt lv c, evaluates_list lt lv -> evaluates (capply c lt) (c_capply c lv)
| FAPPLY : forall lt lv f v i s t, evaluates_list lt lv -> 
           first_rule (f, lv) = Some (i, s, t) -> 
           evaluates t v ->
           evaluates (fapply f lt) v
with evaluates_list : list term -> list value -> Prop :=
| E_nil : evaluates_list [] []
| E_cons : forall t v lt lv, evaluates t v -> evaluates_list lt lv -> evaluates_list (t :: lt) (v :: lv).

Scheme evaluates_mut := Induction for evaluates Sort Prop
with evaluates_list_mut := Induction for evaluates_list Sort Prop.

Lemma evaluates_ind2 : forall P,
(forall lt lv c, Forall2 evaluates lt lv ->
                 Forall2 P lt lv ->
                 P (capply c lt) (c_capply c lv)) ->
(forall lt lv f i s v t,
  Forall2 evaluates lt lv -> Forall2 P lt lv ->
  first_rule (f, lv) = Some (i, s, t) ->
  evaluates t v -> P t v ->
  P (fapply f lt) v) ->
forall (t : term) (v : value), evaluates t v -> P t v.
Proof.
(* Goal: forall (P : forall (_ : Syntax.term variable function constructor) (_ : Syntax.value constructor), Prop) (_ : forall (lt : list (Syntax.term variable function constructor)) (lv : list (Syntax.value constructor)) (c : constructor) (_ : @Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) evaluates lt lv) (_ : @Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) P lt lv), P (@capply variable function constructor c lt) (@c_capply constructor c lv)) (_ : forall (lt : list (Syntax.term variable function constructor)) (lv : list (Syntax.value constructor)) (f : function) (i : nat) (s : forall _ : variable, Syntax.value constructor) (v : Syntax.value constructor) (t : Syntax.term variable function constructor) (_ : @Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) evaluates lt lv) (_ : @Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) P lt lv) (_ : @eq (option (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor))) (first_rule (@pair function (list (Syntax.value constructor)) f lv)) (@Some (prod (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor)) (@pair (prod nat (forall _ : variable, Syntax.value constructor)) (Syntax.term variable function constructor) (@pair nat (forall _ : variable, Syntax.value constructor) i s) t))) (_ : evaluates t v) (_ : P t v), P (@fapply variable function constructor f lt) v) (t : Syntax.term variable function constructor) (v : Syntax.value constructor) (_ : evaluates t v), P t v *)
intros P Hc Hf t v He.
induction He using evaluates_mut with (P := fun t v H => P t v)
(P0 := fun lt lv H => Forall2 P lt lv /\ Forall2 evaluates lt lv).
- apply Hc; tauto.
- eapply Hf; eauto; tauto.
- auto.
- split; constructor; auto; tauto.
Qed.

Inductive Forall2' (A B : Type) (R : A -> B -> Type) : list A -> list B -> Type :=
    Forall2'_nil : Forall2' R [] []
  | Forall2'_cons : forall (x : A) (y : B) (l : list A) (l' : list B),
                   R x y -> Forall2' R l l' -> Forall2' R (x :: l) (y :: l').

Lemma Forall2_trans_rel (A : Type) (R1 R2 : A -> A -> Prop) (l1 l2 : list A) : (forall x y, R1 x y -> R2 x y) -> Forall2 R1 l1 l2 -> Forall2 R2 l1 l2.
Proof.
(* Goal: forall (_ : forall (x y : A) (_ : R1 x y), R2 x y) (_ : @Forall2 A A R1 l1 l2), @Forall2 A A R2 l1 l2 *)
intros H Hall.
(* Goal: and (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) P (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) evaluates (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) *)
induction Hall; auto.
Qed.

Lemma Forall2_product (A : Type) (R : A -> A -> Prop) (ls lt : list A) :
  ls <>  [] -> Forall2 R ls lt -> product R ls lt.
Proof.
(* Goal: and (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) P (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) evaluates (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) *)
induction ls; intros Hnil Hall; try tauto.
clear Hnil.
destruct lt as [ | b lt]; [inversion Hall |].
inversion Hall; subst.
(* Goal: le (suml (@nil nat)) (suml (@nil nat)) *)
constructor 2; trivial.
eapply Forall2_trans_rel.
- intros; constructor; exact H.
- trivial.
Qed.

Lemma Forall2_eq A (l1 l2 : list A) :
  Forall2 eq l1 l2 -> l1 = l2.
Proof.
(* Goal: le (suml (@nil nat)) (suml (@nil nat)) *)
intro H; induction H; subst; trivial.
Qed.

Lemma evaluates_unique t v1 v2 :
  evaluates t v1 ->
  evaluates t v2 ->
  v1 = v2.
Proof.
(* Goal: forall (_ : evaluates t v1) (_ : evaluates t v2), @eq (Syntax.value constructor) v1 v2 *)
intro H1; revert v2.
(* Goal: forall (v2 : Syntax.value constructor) (_ : evaluates t v2), @eq (Syntax.value constructor) v1 v2 *)
induction H1 using evaluates_ind2.
- intros v2 H2.
(* Goal: @eq (Syntax.value constructor) (@c_capply constructor c lv) v2 *)
  inversion H2; subst; clear H2.
(* Goal: @eq (Syntax.value constructor) (@c_capply constructor c lv) (@c_capply constructor c lv0) *)
  f_equal; revert lv0 H5.
(* Goal: le (suml (@nil nat)) (suml (@nil nat)) *)
  induction H; intros lv0 Hlv0; inversion Hlv0; trivial.
(* Goal: @eq (list (Syntax.value constructor)) (@cons (Syntax.value constructor) y l') (@cons (Syntax.value constructor) v lv) *)
  subst.
(* Goal: and (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) P (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) evaluates (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) *)
  f_equal; inversion H0; subst; auto.
- intros v2 Hv2.
(* Goal: @eq (Syntax.value constructor) v v2 *)
  inversion Hv2; subst; clear Hv2.
  assert (Heq : lv = lv0) by
   (clear H6 H1; revert lv0 H5;
    induction H; intros lv0 Hlv0; inversion Hlv0; trivial;
    subst; f_equal; inversion H0; subst; auto).
(* Goal: @eq (Syntax.value constructor) v v2 *)
  subst lv0.
(* Goal: @eq (list (Syntax.value constructor)) (@cons (Syntax.value constructor) y l') (@cons (Syntax.value constructor) v lv) *)
  rewrite H6 in H1; inversion H1; subst.
(* Goal: @eq (Syntax.value constructor) v v2 *)
  now apply IHevaluates.
Qed.

Lemma evaluates_value v : 
  evaluates (term_from_value _ _ v) v.
Proof.
(* Goal: evaluates (@term_from_value variable function constructor v) v *)
induction v using value_ind2.
(* Goal: evaluates (@term_from_value variable function constructor (@c_capply constructor c l)) (@c_capply constructor c l) *)
constructor.
induction l as [|v lv]; constructor; auto with *.
Qed.

Lemma In_nth:
  forall (A : Type) (l : list A) (x d : A) n,
  n < length l -> nth n l d = x -> x ∈ l.
Proof.
(* Goal: forall (A : Type) (l : list A) (x d : A) (n : nat) (_ : lt n (@length A l)) (_ : @eq A (@nth A n l d) x), @In A x l *)
intros A l x d n.
(* Goal: forall (_ : lt n (@length A l)) (_ : @eq A (@nth A n l d) x), @In A x l *)
revert l.
induction n; intros [ | a l];
(* Goal: lt (S i') (S (@length (Syntax.rule variable function constructor) prog')) *)
unfold nth; simpl; intros; try tauto; try omega.
auto with *.
Qed.

Lemma evaluates_sound t v c:
  (forall (t0 : term) (v0 : value), assoc_cache t0 c = Some v0 
    -> evaluates t0 v0 /\ max_arity_term (term_from_value variable function v0) <= max_arity) ->
  evaluates t v ->
  max_arity_term t <= max_arity ->
  exists p, wf p /\ proj_right p = v /\ proj_left p = t /\ cache_left p = c /\
            max_arity_term (term_from_value variable function v) <= max_arity /\
   (forall t0 v0, assoc_cache t0 (cache_right p) = Some v0
      -> evaluates t0 v0 /\ max_arity_term (term_from_value variable function v0) <= max_arity).
Proof.
intros Hc Heval.
revert c Hc.
induction Heval using evaluates_ind2; intros c0 Hc0 Harity.
- assert (Hlp : exists lp c1,
    andl (map wf lp) /\ map (@proj_left _ _ _) lp = lt /\
    map (@proj_right _ _ _) lp = lv /\
    cache_path variable_eq_dec function_eq_dec constructor_eq_dec c0 c1 lp = true /\
    maxl (map (@max_arity_term _ _ _) (map (@term_from_value variable function _) lv)) <= max_arity /\
    forall (t0 : term) (v : value), assoc_cache t0 c1 = Some v -> evaluates t0 v 
        /\ max_arity_term (term_from_value variable function v) <= max_arity
    ).
  { assert (Harityall: forall t, In t lt -> max_arity_term t <= max_arity) by
    ( intros t Ht; simpl in Harity; apply Max.max_lub_r in Harity;
      etransitivity; [ | apply Harity]; now apply maxl_is_max, in_map).
    clear Harity H.
    revert c0 lv H0 Hc0.
    induction lt using rev_ind; intros c0 lv H0 Hc0.
   - exists []; exists c0; simpl.
     inversion H0.
     simpl; intuition.
     now rewrite cache_beq_refl.
   - apply Forall2_app_inv_l in H0.
     destruct H0 as (lv' & ly & Hlt & Hx & Heq).
     subst lv.
(* Goal: @eq (list (Syntax.value constructor)) (@cons (Syntax.value constructor) y l') (@cons (Syntax.value constructor) v lv) *)
     inversion Hx; subst.
     inversion H3; subst; clear H3.
     destruct IHlt with (c0 := c0) (lv := lv') as (lp & c' & Hlp);
     auto with *.
     decompose record Hlp.
     destruct H1  with (c:= c') as [p Hp]; auto with *.
     exists (lp ++ [p]); exists (cache_right p).
(* Goal: @eq (list (Syntax.value constructor)) (@cons (Syntax.value constructor) y l') (@cons (Syntax.value constructor) v lv) *)
     decompose record Hp; subst.
     rewrite map_app, cache_path_app, andl_app.
     repeat rewrite map_app.
     simpl; repeat rewrite cache_beq_refl.
(* Goal: and (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) P (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) evaluates (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) *)
     repeat split; try tauto.
     + rewrite maxl_app.
(* Goal: le (suml (@nil nat)) (suml (@nil nat)) *)
       apply Nat.max_lub; trivial.
(* Goal: le (Nat.max (@max_arity_term variable function constructor t) n) (Nat.max (@max_arity_rule variable function constructor (@rule_intro variable function constructor f lp t)) n) *)
       simpl.
       now rewrite Max.max_0_r.
     + now apply H12.
     + now apply H12 in H0.
  }
  destruct Hlp as [lp Hlp]; decompose record Hlp.
(* Goal: le (Nat.max (@max_arity_term variable function constructor t) n) (Nat.max (@max_arity_rule variable function constructor (@rule_intro variable function constructor f lp t)) n) *)
  eexists (cbv_constr  _ _ (capply c lt) _ (c_capply c lv)); simpl.
(* Goal: and (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) P (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) evaluates (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) *)
  repeat split; eauto.
  + erewrite <- map_length; rewrite H1.
    now apply Max.max_lub_l in Harity.
  + apply Nat.max_lub; trivial.
    rewrite map_length.
    apply Max.max_lub_l in Harity.
    subst lv lt.
    now rewrite map_length in *.
  + now apply H7.
  + edestruct H7; eauto.
- assert (Hlp : exists lp c1,
    andl (map wf lp) /\ map (@proj_left _ _ _) lp = lt /\
    map (@proj_right _ _ _) lp = lv /\
    cache_path variable_eq_dec function_eq_dec constructor_eq_dec c0 c1 lp = true /\
    maxl (map (@max_arity_term _ _ _) (map (@term_from_value variable function _) lv)) <= max_arity /\
    forall (t0 : term) (v : value), assoc_cache t0 c1 = Some v -> evaluates t0 v
    /\ max_arity_term (term_from_value variable function v) <= max_arity

    ).
  { assert (Harityall: forall t, In t lt -> max_arity_term t <= max_arity) by
    ( intros t0 Ht; simpl in Harity; apply Max.max_lub_r in Harity;
      etransitivity; [ | apply Harity]; now apply maxl_is_max, in_map).
    clear Harity H1 H.
    revert c0 lv H0 Hc0.
    induction lt using rev_ind; intros c0 lv H0 Hc0.
   - exists []; exists c0; simpl.
     inversion H0.
     simpl; intuition.
     now rewrite cache_beq_refl.
   - apply Forall2_app_inv_l in H0.
     destruct H0 as (lv' & ly & Hlt & Hx & Heq).
     subst lv.
(* Goal: @eq (list (Syntax.value constructor)) (@cons (Syntax.value constructor) y l') (@cons (Syntax.value constructor) v lv) *)
     inversion Hx; subst.
     inversion H3; subst; clear H3.
     destruct IHlt with (c0 := c0) (lv := lv') as (lp & c' & Hlp);
     auto with *.
     decompose record Hlp.
     destruct H1  with (c:= c') as [p Hp]; auto with *.
     exists (lp ++ [p]); exists (cache_right p).
(* Goal: @eq (list (Syntax.value constructor)) (@cons (Syntax.value constructor) y l') (@cons (Syntax.value constructor) v lv) *)
     decompose record Hp; subst.
     rewrite map_app, cache_path_app, andl_app.
     repeat rewrite map_app.
     simpl; repeat rewrite cache_beq_refl.
(* Goal: and (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) P (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) evaluates (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) *)
     repeat split; try tauto.
     + rewrite maxl_app.
(* Goal: le (suml (@nil nat)) (suml (@nil nat)) *)
       apply Nat.max_lub; trivial.
(* Goal: le (Nat.max (@max_arity_term variable function constructor t) n) (Nat.max (@max_arity_rule variable function constructor (@rule_intro variable function constructor f lp t)) n) *)
       simpl.
       now rewrite Max.max_0_r.
     + now apply H12.
     + now apply H12 in H0.
  }
  destruct Hlp as (lp & cr & Hlp); decompose record Hlp.
  case_eq (assoc (term_beq variable_eq_dec function_eq_dec constructor_eq_dec) (fapply f (map (@term_from_value _ _ _) lv)) cr).
  + intros v0 Hv0.
    destruct (H8 _ _ Hv0) as [Heval0 Harity0].
    eexists (cbv_split _ (cbv_read _ (fapply f _) _) _ _ _ _).
(* Goal: @eq (list (Syntax.value constructor)) (@cons (Syntax.value constructor) y l') (@cons (Syntax.value constructor) v lv) *)
    subst.
    assert (v0 = v).
(* Goal: forall (x : variable) (_ : @In variable x (@vars_of_term variable function constructor t)), le (@max_arity_term variable function constructor (@term_from_value variable function constructor (s x))) (@max_arity_term variable function constructor t') *)
(* Goal: le (@max_arity_term variable function constructor (@subst variable function constructor s t)) (Nat.max (@max_arity_rule variable function constructor (@rule_intro variable function constructor f lp t)) (@max_arity_term variable function constructor t')) *)
    { eapply evaluates_unique; eauto.
(* Goal: and (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) P (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) evaluates (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) *)
      econstructor; eauto.
      clear H H1 H0 H2 H5 H6 Hv0 H8 Hlp cr IHHeval Harity Heval0.
(* Goal: le (suml (@nil nat)) (suml (@nil nat)) *)
      induction lp; constructor; trivial.
      apply evaluates_value.
    }
    subst v0.
(* Goal: and (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) P (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) evaluates (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) *)
    repeat split; trivial;simpl; repeat split; eauto.
    * apply Max.max_lub_l in Harity.
      now rewrite map_length in Harity.
    * now apply H8.
    * now apply H8 in H3.
  + assert(Hrule := H1).
    apply first_rule_sound in H1.
    destruct H1 as [[lp' t'] (Hlen & Hnth & Hunify & Hsubst)].
(* Goal: le (suml (@nil nat)) (suml (@nil nat)) *)
    destruct IHHeval with cr as [p Hp]; trivial.
    * unfold wf_prog in prog_is_wf; destruct prog_is_wf as (Hvars & Hmaxarity).
(* Goal: active_term_order_superset (@pair function (list (Syntax.value constructor)) f lv) (@pair function (list (Syntax.value constructor)) f' lv') *)
      subst t.
(* Goal: le (suml (@nil nat)) (suml (@nil nat)) *)
      apply first_rule_max_arity in Hrule; trivial.
      simpl; rewrite map_length.
(* Goal: le (suml (@nil nat)) (suml (@nil nat)) *)
      apply Nat.max_lub; trivial.
      subst lv lt.
      apply Nat.max_lub_l in Harity.
      now rewrite map_length in *.
    * intro Hcache.
      decompose record Hp; decompose record Hlp.
      set (tt := fapply f(map (term_from_value variable function (constructor:=constructor)) (map (psubst s) lp'))).
      eexists (cbv_split lp (cbv_update i s p cr (fapply f _) ((tt, v) :: (cache_right p)) v) _ (fapply f lt) ((tt, v):: (cache_right p)) v).
(* Goal: @eq (list (Syntax.value constructor)) (@cons (Syntax.value constructor) y l') (@cons (Syntax.value constructor) v lv) *)
      simpl; subst.
      assert(Hlp_len : length lp <= max_arity) by
      (simpl in Harity; rewrite map_length in Harity; lia).
      apply unify_list_sound in Hunify.
      rewrite <- H7 in *; simpl.
(* Goal: and (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) P (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) evaluates (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) *)
      repeat split; auto.
      -- subst tt; exists lp'; rewrite Hunify.
(* Goal: and (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) P (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) (@Forall2 (Syntax.term variable function constructor) (Syntax.value constructor) evaluates (@nil (Syntax.term variable function constructor)) (@nil (Syntax.value constructor))) *)
         eexists; repeat split; eauto; try tauto.
         now repeat rewrite map_length.
      -- intros.
         case_eq (term_beq variable_eq_dec function_eq_dec constructor_eq_dec t0 tt).
         ++ intro Heq; rewrite term_beq_eq in Heq; subst t0.
            replace (term_beq variable_eq_dec function_eq_dec constructor_eq_dec tt tt) with true in H1 by
            (symmetry; now apply term_beq_eq).
            subst tt.
(* Goal: le (suml (@nil nat)) (suml (@nil nat)) *)
            eapply FAPPLY with (lv := (map (proj_right (constructor:=constructor)) lp)) (i := i) (s := s) (t := proj_left p); trivial.
            ** rewrite Hunify.
               clear H6 H3 H0 H1 Hcache Hlp H5 H6 H7 H11 H12 H13 H16 H14 H2 Harity H Hunify Hlp_len Hrule.
(* Goal: evaluates (@term_from_value variable function constructor (@c_capply constructor c l)) (@c_capply constructor c l) *)
               induction lp; constructor.
               apply evaluates_value.
(* Goal: le (suml (@nil nat)) (suml (@nil nat)) *)
               apply IHlp; trivial.
               simpl in H17.
               now apply Nat.max_lub_r in H17.
            ** assert( Hbeq : forall t, term_beq variable_eq_dec function_eq_dec constructor_eq_dec t t = true) by
               (now intros; rewrite term_beq_eq).
               rewrite Hbeq in H3.
               now inversion H3.
         ++ intro Heq; rewrite Heq in H3.
            now apply H13.
      -- case_eq (term_beq variable_eq_dec function_eq_dec constructor_eq_dec t0 tt).
         ++ intro Heq; rewrite Heq in H3; inversion H3; now subst.
         ++ intro Hneq; rewrite Hneq in H3.
            now apply H13 in H3.
Qed.

(* Simpler, weaker version *)
Lemma evaluates_sound' (t : term) (v : value):
  evaluates t v ->
  max_arity_term t <= max_arity ->
  exists p, wf p /\ proj_right p = v /\ proj_left p = t.
Proof.
(* Goal: forall (_ : evaluates t v) (_ : le (@max_arity_term variable function constructor t) max_arity), @ex (CBV_cache.cbv variable function constructor) (fun p : CBV_cache.cbv variable function constructor => and (@CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p) (and (@eq (Syntax.value constructor) (@proj_right variable function constructor p) v) (@eq (Syntax.term variable function constructor) (@proj_left variable function constructor p) t))) *)
intros.
(* Goal: le (suml (@nil nat)) (suml (@nil nat)) *)
destruct (@evaluates_sound t v []); trivial.
- intros t' v' Hf; inversion Hf.
- intuition; eexists; eauto.
Qed.

End Evaluates.

Create HintDb eval.

Ltac reduce := 
  progress (repeat constructor) ||
  (econstructor; [repeat constructor; repeat reduce; eauto with eval
                              | solve [unfold first_rule; simpl; trivial]
                              | unfold assoc_default; repeat constructor; eauto with eval]).

Hint Extern 1 (@evaluates _ _ _ _ _ _ _ _ _ _)  => eapply evaluates_value: eval.
