Require Import Le Max List Bool Cecoa.Lib Cecoa.Syntax Cecoa.CBV_cache NPeano Omega Cecoa.OptionMonad.

Section QI.

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 term_from_value := (Syntax.term_from_value variable function (constructor:=constructor)).
Notation term_from_pattern := (Syntax.term_from_pattern (variable:=variable) function (constructor:=constructor)).
Variable prog : list rule.
Variable max_arity:nat.
Variable rule_default : rule.

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}.

Notation cache := (CBV_cache.cache variable function constructor).
Notation cache_path := (CBV_cache.cache_path variable_eq_dec function_eq_dec constructor_eq_dec).



Notation cache_path_transitivity := 
           (@CBV_cache.cache_path_transitivity _ _ _ variable_eq_dec function_eq_dec constructor_eq_dec).
Notation cache_path_transitivity_left :=
           (@CBV_cache.cache_path_transitivity_left _ _ _ variable_eq_dec function_eq_dec constructor_eq_dec).
Notation cbv := (CBV_cache.cbv variable function constructor).
Notation wf := (CBV_cache.wf variable_eq_dec  function_eq_dec constructor_eq_dec rule_default
                prog max_arity).

(*Definition 11*)
Definition assignment_constructor := constructor -> list nat -> nat.
Definition assignment_function := function -> list nat -> nat.

(*****************************************************************************************)
(*                  QI of constructors / value                                           *)
(*****************************************************************************************)

(* additivity*)
Variable mcs: nat.

Definition constructor_non_zero cs :=
   forall c:constructor, cs  c > 0. 

Definition additive (qic:assignment_constructor) cs :=
   forall c:constructor, forall l, qic c l=(suml l)+(cs c).

Definition mcs_is_max_constructor_size cs :=
    forall c:constructor, cs c <= mcs.

Lemma monotonicity_qic qic cs: additive qic cs -> forall c:constructor,
  forall lx ly, Forall2 le lx ly -> qic c lx <= qic c ly.
Proof.
(* Goal: forall (_ : additive qic cs) (c : constructor) (lx ly : list nat) (_ : @Forall2 nat nat le lx ly), le (qic c lx) (qic c ly) *)
intro additivity;intros.
(* Goal: forall v : Syntax.value constructor, le (value_assignment qic v) (Init.Nat.mul mcs (@value_size constructor v)) *)
unfold additive in additivity.
(* Goal: le (qic c lx) (qic c ly) *)
rewrite additivity;rewrite additivity.
(* Goal: le (Init.Nat.add (suml lx) (cs c)) (Init.Nat.add (suml ly) (cs c)) *)
apply Plus.plus_le_compat_r;trivial.
(* Goal: le (suml lx) (suml ly) *)
induction H;auto;simpl.
(* Goal: le (Init.Nat.add x (suml l)) (Init.Nat.add y (suml l')) *)
apply Plus.plus_le_compat;trivial.
Qed.

(* assignment of a value*)
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
Fixpoint value_assignment (qic:assignment_constructor) (v:value) {struct v}:=
   match v with
  | c_capply c lv => qic c (map (value_assignment qic) lv)
   end.

(*Lemma 67 borne inf *)
Lemma value_size_le_QI qic cs: 
  additive qic cs -> constructor_non_zero cs ->
  forall v:value, value_size v <= value_assignment qic v.
Proof.
(* Goal: forall (_ : additive qic cs) (_ : constructor_non_zero cs) (v : Syntax.value constructor), le (@value_size constructor v) (value_assignment qic v) *)
intros additivity non_zero.
(* Goal: forall v : Syntax.value constructor, le (value_assignment qic v) (Init.Nat.mul mcs (@value_size constructor v)) *)
unfold additive in additivity. unfold constructor_non_zero in non_zero.
(* Goal: forall v : Syntax.value constructor, @eq (option nat) (p_term_assignment qic qif (@Syntax.term_from_value variable function constructor v)) (@Some nat (value_assignment qic v)) *)
induction v using value_ind2.
(* Goal: @eq (option nat) (p_term_assignment qic qif (@Syntax.term_from_value variable function constructor (@c_capply constructor c l))) (@Some nat (value_assignment qic (@c_capply constructor c l))) *)
simpl.
(* Goal: le (S (suml (@map (Syntax.value constructor) nat (@value_size constructor) l))) (qic c (@map (Syntax.value constructor) nat (value_assignment qic) l)) *)
apply le_trans with (m:=suml (map (value_assignment qic) l)+1).
- apply le_trans with (m:=S (suml (map (value_assignment qic) l)));try omega. (* j'ai du mal avec S/+1 *)
  rewrite <- Nat.succ_le_mono.
(* Goal: le (suml (@map (Syntax.value constructor) nat (value_assignment qic) l)) (suml (@map (Syntax.value constructor) nat (fun x : Syntax.value constructor => Init.Nat.mul mcs (@value_size constructor x)) l)) *)
  apply suml_map_le;trivial.
- rewrite additivity.
(* Goal: le (Init.Nat.add (@term_size variable function constructor s) (value_assignment qic u)) (Init.Nat.add (@term_size variable function constructor s) (term_assignment qic qif s)) *)
  apply Plus.plus_le_compat_l.
(* Goal: le (S O) (cs c) *)
  apply (non_zero c).
Qed.

(*Lemma 67 borne sup *)
Lemma QI_le_value_size qic cs: 
  additive qic cs -> mcs_is_max_constructor_size cs ->
  forall v:value, 
  value_assignment qic v <= mcs*(value_size v).
Proof.
(* Goal: forall (_ : additive qic cs) (_ : mcs_is_max_constructor_size cs) (v : Syntax.value constructor), le (value_assignment qic v) (Init.Nat.mul mcs (@value_size constructor v)) *)
intros additivity max_cs.
(* Goal: forall v : Syntax.value constructor, le (value_assignment qic v) (Init.Nat.mul mcs (@value_size constructor v)) *)
unfold additive in additivity. unfold mcs_is_max_constructor_size in max_cs.
(* Goal: forall v : Syntax.value constructor, @eq (option nat) (p_term_assignment qic qif (@Syntax.term_from_value variable function constructor v)) (@Some nat (value_assignment qic v)) *)
induction v using value_ind2.
(* Goal: @eq (option nat) (p_term_assignment qic qif (@Syntax.term_from_value variable function constructor (@c_capply constructor c l))) (@Some nat (value_assignment qic (@c_capply constructor c l))) *)
simpl.
(* Goal: le (qic c (@map (Syntax.value constructor) nat (value_assignment qic) l)) (Init.Nat.mul mcs (S (suml (@map (Syntax.value constructor) nat (@value_size constructor) l)))) *)
rewrite additivity.
(* Goal: le (Init.Nat.add (suml (@map (Syntax.value constructor) nat (value_assignment qic) l)) (cs c)) (Init.Nat.mul mcs (S (suml (@map (Syntax.value constructor) nat (@value_size constructor) l)))) *)
apply le_trans with (m:=suml (map (value_assignment qic) l)+mcs).
- apply Plus.plus_le_compat_l.
(* Goal: le (cs c) mcs *)
  apply max_cs.
- replace (S (suml (map (value_size (constructor:=constructor)) l))) 
          with ((suml (map (value_size (constructor:=constructor)) l)+1));try omega.
  (* comment remplacer automatiquement S x par x+1 pour pouvoir appliquer la distributivité ? *)
(* Goal: le (Init.Nat.add (suml (@map (Syntax.value constructor) nat (value_assignment qic) l)) mcs) (Init.Nat.mul mcs (Init.Nat.add (suml (@map (Syntax.value constructor) nat (@value_size constructor) l)) (S O))) *)
  rewrite Mult.mult_plus_distr_l;rewrite Mult.mult_1_r;apply Plus.plus_le_compat_r.
(* Goal: le (suml (@map (Syntax.value constructor) nat (value_assignment qic) l)) (Nat.mul mcs (suml (@map (Syntax.value constructor) nat (@value_size constructor) l))) *)
  rewrite mult_suml_r;rewrite map_map.
(* Goal: le (suml (@map (Syntax.value constructor) nat (value_assignment qic) l)) (suml (@map (Syntax.value constructor) nat (fun x : Syntax.value constructor => Init.Nat.mul mcs (@value_size constructor x)) l)) *)
  apply suml_map_le;trivial.
Qed.

(*****************************************************************************************)
(*                  QI of function symbols / terms                                       *)
(*****************************************************************************************)

(* c'est cette forme qui est utilisée partout *)
Definition subterm (qif:assignment_function) := forall f l x, In x l -> x <= qif f l.

(*monotonicity*)
Definition monotonicity_qif (qif:assignment_function) :=
  forall f lx ly, Forall2 le lx ly -> qif f lx <= qif f ly.



(* assignment of a term*)
Fixpoint term_assignment (qic:assignment_constructor) (qif:assignment_function)
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
(t:term) {struct t}:=
   match t with
  | var v=> 0 (* pas necessaire. Les QI sont toujours appliquées sur des termes clots. *)
  | capply c lt => qic c (map (term_assignment qic qif) lt)
  | fapply f lt=> qif f (map (term_assignment qic qif)  lt) 
 end.

(*Definition 12*)
Definition compatible_QI qic qif := forall f lp t, forall s:variable -> value,
  let ru := rule_intro f lp t in (* f(p1, ..., pn) -> t *)
  (In ru prog) -> 
  term_assignment qic qif (subst s t) <= term_assignment qic qif (subst s (lhs_of_rule ru)). 
  (* pour toute substitution, QI(t) <= QI(f(p1, ..., pn)) *)

Definition valid_QI qic qif cs :=
  (additive qic cs) /\ (mcs_is_max_constructor_size cs) /\ (constructor_non_zero cs) /\
  (subterm qif) /\ (monotonicity_qif qif) /\ (compatible_QI qic qif).

Definition cache_bounded qic qif (c:cache): Prop  := 
  Forall (fun t => value_assignment qic (snd t) <= term_assignment qic qif (fst t)) c.

(* sous typage *)
Lemma value_as_term_assignment qic qif: forall v:value,
  (term_assignment qic qif (term_from_value v)) = (value_assignment qic v).
Proof.
(* Goal: forall v : Syntax.value constructor, @eq (option nat) (p_term_assignment qic qif (@Syntax.term_from_value variable function constructor v)) (@Some nat (value_assignment qic v)) *)
induction v using value_ind2.
(* Goal: @eq (option nat) (p_term_assignment qic qif (@Syntax.term_from_value variable function constructor (@c_capply constructor c l))) (@Some nat (value_assignment qic (@c_capply constructor c l))) *)
simpl.
(* Goal: @eq (option nat) match (fix option_list_map (A : Type) (l : list (option A)) {struct l} : option (list A) := match l with | nil => @Some (list A) (@nil A) | cons (Some h as o) t => @option_map (list A) (list A) (@cons A h) (option_list_map A t) | cons (None as o) t => @None (list A) end) nat (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic qif) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor) l)) with | Some a => @Some nat (qic c a) | None => @None nat end (@Some nat (qic c (@map (Syntax.value constructor) nat (value_assignment qic) l))) *)
rewrite map_map.
(* Goal: @eq nat (qic c (@map (Syntax.value constructor) nat (fun x : Syntax.value constructor => term_assignment qic qif (@Syntax.term_from_value variable function constructor x)) l)) (qic c (@map (Syntax.value constructor) nat (value_assignment qic) l)) *)
apply f_equal2;trivial.
(* Goal: @eq (list nat) (@map (Syntax.value constructor) nat (fun x : Syntax.value constructor => term_assignment qic qif (@Syntax.term_from_value variable function constructor x)) l) (@map (Syntax.value constructor) nat (value_assignment qic) l) *)
apply map_in_ext;trivial.
Qed.


(*****************************************************************************************)
(*                        starting real proofs                                           *)
(*****************************************************************************************)

(* Les 2 lemmes suivants sont utilisés 2 fois par la suite. *)
Lemma qi_fapply_right_le_qi_fapply_left qic qif : forall proof_tree lp f c1,
  monotonicity_qif qif ->
  let l := map (proj_left (constructor:=constructor)) lp in
  let l' := map term_from_value (map (proj_right (constructor:=constructor)) lp) in
  let c := cache_left proof_tree in let v := proj_right proof_tree in
  (forall p, In p lp -> cache_bounded qic qif (cache_left p) -> 
             value_assignment qic (proj_right p) <= term_assignment qic qif (proj_left p) /\ 
             cache_bounded qic qif (cache_right p)) ->
  cache_bounded qic qif c1 -> cache_path c1 c lp = true -> andl (map wf lp) -> 
  (term_assignment qic qif (fapply f l')) <= (term_assignment qic qif (fapply f l)).
Proof.
(* Goal: forall (proof_tree : CBV_cache.cbv variable function constructor) (lp : list (CBV_cache.cbv variable function constructor)) (f : function) (c1 : CBV_cache.cache variable function constructor) (_ : monotonicity_qif qif), let l := @map (CBV_cache.cbv variable function constructor) (Syntax.term variable function constructor) (@proj_left variable function constructor) lp in let l' := @map (Syntax.value constructor) (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor) (@map (CBV_cache.cbv variable function constructor) (Syntax.value constructor) (@proj_right variable function constructor) lp) in let c := @cache_left variable function constructor proof_tree in let v := @proj_right variable function constructor proof_tree in forall (_ : forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : cache_bounded qic qif (@cache_left variable function constructor p)), and (le (value_assignment qic (@proj_right variable function constructor p)) (term_assignment qic qif (@proj_left variable function constructor p))) (cache_bounded qic qif (@cache_right variable function constructor p))) (_ : cache_bounded qic qif c1) (_ : @eq bool (@CBV_cache.cache_path variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec c1 c lp) true) (_ : andl (@map (CBV_cache.cbv variable function constructor) Prop (@CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity) lp)), le (term_assignment qic qif (@fapply variable function constructor f l')) (term_assignment qic qif (@fapply variable function constructor f l)) *)
intros proof_tree lp f c1 monotonicity l l' c v.
(* Goal: forall (_ : forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : cache_bounded qic qif (@cache_left variable function constructor p)), and (le (value_assignment qic (@proj_right variable function constructor p)) (term_assignment qic qif (@proj_left variable function constructor p))) (cache_bounded qic qif (@cache_right variable function constructor p))) (_ : cache_bounded qic qif c1) (_ : @eq bool (@CBV_cache.cache_path variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec c1 c lp) true) (_ : andl (@map (CBV_cache.cbv variable function constructor) Prop (@CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity) lp)), le (term_assignment qic qif (@fapply variable function constructor f l')) (term_assignment qic qif (@fapply variable function constructor f l)) *)
intros lp_bound c1_bound c_path wf_lp.
(* Goal: @eq (option nat) (p_term_assignment qic qif (@Syntax.term_from_value variable function constructor (@c_capply constructor c l))) (@Some nat (value_assignment qic (@c_capply constructor c l))) *)
simpl.
(* Goal: le (qif f (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l')) (qif f (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l)) *)
unfold monotonicity_qif in monotonicity.
(* Goal: le (qif f (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l')) (qif f (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l)) *)
apply monotonicity.
(* Goal: @Forall2 nat nat le (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l') (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l) *)
unfold l;unfold l';clear l l'.
(* Goal: @eq (option nat) match (fix option_list_map (A : Type) (l : list (option A)) {struct l} : option (list A) := match l with | nil => @Some (list A) (@nil A) | cons (Some h as o) t => @option_map (list A) (list A) (@cons A h) (option_list_map A t) | cons (None as o) t => @None (list A) end) nat (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic qif) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor) l)) with | Some a => @Some nat (qic c a) | None => @None nat end (@Some nat (qic c (@map (Syntax.value constructor) nat (value_assignment qic) l))) *)
rewrite map_map;rewrite map_map;rewrite map_map.
(* Goal: @Forall2 nat nat le (@map (Syntax.term variable function constructor) nat (fun v : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor v)) lt) (@map (Syntax.term variable function constructor) nat (fun _ : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor t)) lt) *)
apply Forall2_map.
(* Goal: forall _ : le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)))), le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (Datatypes.S O)) (qif f l)) (Datatypes.S O)) *)
intros.
(* Goal: le (@value_size constructor x0) (term_assignment qic qif (@Syntax.term_from_value variable function constructor x0)) *)
rewrite value_as_term_assignment.
(* Goal: le (value_assignment qic (@proj_right variable function constructor x)) (term_assignment qic qif (@proj_left variable function constructor x)) *)
apply lp_bound;auto.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor x) *)
apply cache_path_transitivity_left with (c:=c1) (c':=c) (l:=lp);auto.
(* Goal: forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : cache_bounded qic qif (@cache_left variable function constructor p)), cache_bounded qic qif (@cache_right variable function constructor p) *)
apply lp_bound.
Qed.

Lemma qi_right_le_qi_fapply_left qic qif: forall proof_tree lp f c1,
  monotonicity_qif qif -> wf proof_tree ->
  let l := map (proj_left (constructor:=constructor)) lp in
  let l' := map term_from_value (map (proj_right (constructor:=constructor)) lp) in
  let c := cache_left proof_tree in let c' := cache_right proof_tree in
  let v := proj_right proof_tree in
  proj_left proof_tree = fapply f l' -> 
  (forall p, In p lp -> cache_bounded qic qif (cache_left p) -> wf p ->
             value_assignment qic (proj_right p) <= term_assignment qic qif (proj_left p) /\ 
             cache_bounded qic qif (cache_right p)) ->
  (cache_bounded qic qif c -> value_assignment qic v <= term_assignment qic qif (fapply f l')) ->
  cache_bounded qic qif c1 -> cache_bounded qic qif c' -> cache_path c1 c lp = true ->
    andl (map wf lp) -> 
  value_assignment qic v <= term_assignment qic qif (fapply f l).
Proof.
(* Goal: forall (proof_tree : CBV_cache.cbv variable function constructor) (lp : list (CBV_cache.cbv variable function constructor)) (f : function) (c1 : CBV_cache.cache variable function constructor) (_ : monotonicity_qif qif) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity proof_tree), let l := @map (CBV_cache.cbv variable function constructor) (Syntax.term variable function constructor) (@proj_left variable function constructor) lp in let l' := @map (Syntax.value constructor) (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor) (@map (CBV_cache.cbv variable function constructor) (Syntax.value constructor) (@proj_right variable function constructor) lp) in let c := @cache_left variable function constructor proof_tree in let c' := @cache_right variable function constructor proof_tree in let v := @proj_right variable function constructor proof_tree in forall (_ : @eq (Syntax.term variable function constructor) (@proj_left variable function constructor proof_tree) (@fapply variable function constructor f l')) (_ : forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : cache_bounded qic qif (@cache_left variable function constructor p)) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p), and (le (value_assignment qic (@proj_right variable function constructor p)) (term_assignment qic qif (@proj_left variable function constructor p))) (cache_bounded qic qif (@cache_right variable function constructor p))) (_ : forall _ : cache_bounded qic qif c, le (value_assignment qic v) (term_assignment qic qif (@fapply variable function constructor f l'))) (_ : cache_bounded qic qif c1) (_ : cache_bounded qic qif c') (_ : @eq bool (@CBV_cache.cache_path variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec c1 c lp) true) (_ : andl (@map (CBV_cache.cbv variable function constructor) Prop (@CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity) lp)), le (value_assignment qic v) (term_assignment qic qif (@fapply variable function constructor f l)) *)
intros proof_tree lp f c1 monotonicity well_formed l l' c c' v.
(* Goal: forall (_ : @eq (Syntax.term variable function constructor) (@proj_left variable function constructor proof_tree) (@fapply variable function constructor f l')) (_ : forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : cache_bounded qic qif (@cache_left variable function constructor p)) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p), and (le (value_assignment qic (@proj_right variable function constructor p)) (term_assignment qic qif (@proj_left variable function constructor p))) (cache_bounded qic qif (@cache_right variable function constructor p))) (_ : forall _ : cache_bounded qic qif c, le (value_assignment qic v) (term_assignment qic qif (@fapply variable function constructor f l'))) (_ : cache_bounded qic qif c1) (_ : cache_bounded qic qif c') (_ : @eq bool (@CBV_cache.cache_path variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec c1 c lp) true) (_ : andl (@map (CBV_cache.cbv variable function constructor) Prop (@CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity) lp)), le (value_assignment qic v) (term_assignment qic qif (@fapply variable function constructor f l)) *)
intros pl lp_bound val_bound c1_bound c'_bound c_path wf_lp.
(* Goal: le (value_assignment qic v) (term_assignment qic qif (@fapply variable function constructor f l)) *)
apply le_trans with (m:=term_assignment qic qif (fapply f l'));auto.
- apply val_bound;auto.
(* Goal: cache_bounded qic qif c *)
  apply cache_path_transitivity with (c:=c1) (c':=c) (l:=lp);auto.
(* Goal: le (value_assignment qic (@proj_right variable function constructor x)) (term_assignment qic qif (@proj_left variable function constructor x)) *)
  intros;apply lp_bound;auto.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity a *)
  apply andl_in_map with (l:=lp);auto.
- apply qi_fapply_right_le_qi_fapply_left with (proof_tree:=proof_tree) (c1:=c1);try tauto.
(* Goal: forall _ : le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)))), le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (Datatypes.S O)) (qif f l)) (Datatypes.S O)) *)
  intros.
(* Goal: and (le (value_assignment qic (@proj_right variable function constructor p)) (term_assignment qic qif (@proj_left variable function constructor p))) (cache_bounded qic qif (@cache_right variable function constructor p)) *)
  apply lp_bound;try tauto.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity a *)
  apply andl_in_map with (l:=lp);auto.
Qed.

(* Lemma 68 *)
(* Lemme clé : pour chaque jugement de cache gauche borné,
               * le cache droit est aussi borné.
               * la QI de gauche est plus grande que la QI de droite
*)
Lemma left_bound_to_right_bound qic qif cs:forall pi:cbv,
    valid_QI qic qif cs -> (wf pi) ->
    cache_bounded qic qif (cache_left pi) ->
    (value_assignment qic (proj_right pi) <= term_assignment qic qif (proj_left pi)
     /\ cache_bounded qic qif (cache_right pi)).
Proof.
(* Goal: forall (pi : CBV_cache.cbv variable function constructor) (_ : valid_QI qic qif cs) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity pi) (_ : cache_bounded qic qif (@cache_left variable function constructor pi)), and (le (value_assignment qic (@proj_right variable function constructor pi)) (term_assignment qic qif (@proj_left variable function constructor pi))) (cache_bounded qic qif (@cache_right variable function constructor pi)) *)
intros pi valid.
(* Goal: let t := @fapply variable function constructor f lt in let l := @map (Syntax.term variable function constructor) nat (fun _ : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor t)) lt in forall _ : @eq (list (Syntax.term variable function constructor)) lt (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor) lval), le (term_assignment qic qif t) (qif f l) *)
unfold valid_QI in valid.
(* Goal: forall (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity pi) (_ : cache_bounded qic qif (@cache_left variable function constructor pi)), and (le (value_assignment qic (@proj_right variable function constructor pi)) (term_assignment qic qif (@proj_left variable function constructor pi))) (cache_bounded qic qif (@cache_right variable function constructor pi)) *)
destruct valid as (additivity & mcs_is_max & non_zero & sub & mono & compat).
induction pi using cbv_ind2;
          unfold cache_left;unfold proj_right;unfold proj_left;unfold cache_right;
          intros well_formed cache.
- (* cas cbv_constr *)
(* Goal: and (le (value_assignment qic v) (term_assignment qic qif (@fapply variable function constructor f l))) (cache_bounded qic qif c2) *)
  assert (cache_bounded qic qif c2).
  + (* preuve du assert : borne sur le cache *)
(* Goal: le (value_assignment qic v) (term_assignment qic qif t) *)
    simpl in well_formed;destruct t;destruct v;try tauto.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
    destruct well_formed as (cpath & Hc & Hl & Hl0 & wf_list & arity).
(* Goal: cache_bounded qic qif c2 *)
    apply cache_path_transitivity with (c:=c1) (c':=c2) (l:=lp);auto.
(* Goal: forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : cache_bounded qic qif (@cache_left variable function constructor p)), cache_bounded qic qif (@cache_right variable function constructor p) *)
    intros;apply H;auto.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity a *)
    apply andl_in_map with (l:=lp);auto.
  + (* borne sur les QI *)
(* Goal: and (le (value_assignment qic v) (term_assignment qic qif t)) (cache_bounded qic qif c) *)
    split;auto.
(* Goal: le (value_assignment qic v) (term_assignment qic qif t) *)
    simpl in well_formed;destruct t;destruct v;try tauto.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
    destruct well_formed as (cpath & Hc & Hl & Hl0 & wf_list & arity).
(* Goal: le (value_assignment qic (@c_capply constructor c0 l0)) (term_assignment qic qif (@capply variable function constructor c l)) *)
    subst c.
(* Goal: le (value_assignment qic (@c_capply constructor c0 l0)) (term_assignment qic qif (@capply variable function constructor c0 l)) *)
    simpl;apply (monotonicity_qic qic cs);trivial.
(* Goal: @Forall2 nat nat le (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l) (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l0) *)
    subst l l0.
(* Goal: @eq (option nat) match (fix option_list_map (A : Type) (l : list (option A)) {struct l} : option (list A) := match l with | nil => @Some (list A) (@nil A) | cons (Some h as o) t => @option_map (list A) (list A) (@cons A h) (option_list_map A t) | cons (None as o) t => @None (list A) end) nat (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic qif) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor) l)) with | Some a => @Some nat (qic c a) | None => @None nat end (@Some nat (qic c (@map (Syntax.value constructor) nat (value_assignment qic) l))) *)
    rewrite map_map;rewrite map_map.
(* Goal: @Forall2 nat nat le (@map (Syntax.term variable function constructor) nat (fun v : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor v)) lt) (@map (Syntax.term variable function constructor) nat (fun _ : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor t)) lt) *)
    apply Forall2_map.
(* Goal: forall _ : le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)))), le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (Datatypes.S O)) (qif f l)) (Datatypes.S O)) *)
    intros.
(* Goal: cache_bounded qic qif (@cache_right variable function constructor p) *)
    apply H;auto.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity a *)
    * apply andl_in_map with (l:=lp);auto. 
    * apply cache_path_transitivity_left with (c:=c1) (c':=c2) (l:=lp);auto.
(* Goal: forall _ : le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)))), le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (Datatypes.S O)) (qif f l)) (Datatypes.S O)) *)
      intros.
(* Goal: cache_bounded qic qif (@cache_right variable function constructor p) *)
      apply H;auto.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity a *)
      apply andl_in_map with (l:=lp);auto.
- (* cas cbv_split *)
(* Goal: and (le (value_assignment qic v) (term_assignment qic qif t)) (cache_bounded qic qif c2) *)
  destruct t;simpl in well_formed;destruct pi;destruct t;try tauto.
  + (* cbv_update *)
(* Goal: and (le (value_assignment qic v) (term_assignment qic qif (@fapply variable function constructor f l))) (cache_bounded qic qif c2) *)
    assert (cache_bounded qic qif c2).
    * (* preuve du assert *)
      destruct well_formed as (Hc2 & cpath &  Hl & Hl0 & wf_list & Hf & Hv & well_formed & arity).
(* Goal: le (value_assignment qic v) (term_assignment qic qif (@fapply variable function constructor f l)) *)
      unfold cache_left in IHpi;unfold cache_right in IHpi.
(* Goal: cache_bounded qic qif c2 *)
      subst c2.
(* Goal: @Forall (prod (Syntax.term variable function constructor) (Syntax.value constructor)) (fun t : prod (Syntax.term variable function constructor) (Syntax.value constructor) => le (value_assignment qic (@snd (Syntax.term variable function constructor) (Syntax.value constructor) t)) (term_assignment qic qif (@fst (Syntax.term variable function constructor) (Syntax.value constructor) t))) (@cache_right variable function constructor pi) *)
      apply IHpi;auto.
(* Goal: cache_bounded qic qif c *)
      apply cache_path_transitivity with (c:=c1) (c':=c) (l:=lp);auto.
(* Goal: forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : cache_bounded qic qif (@cache_left variable function constructor p)), cache_bounded qic qif (@cache_right variable function constructor p) *)
      intros;apply H;auto.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity a *)
      apply andl_in_map with (l:=lp);auto.
    * (* borne sur les QI *)
(* Goal: and (le (value_assignment qic v) (term_assignment qic qif t)) (cache_bounded qic qif c) *)
      split;auto.
      destruct well_formed as (Hc2 & cpath &  Hl & Hl0 & wf_list & Hf & Hv & well_formed & arity).
(* Goal: le (value_assignment qic v) (term_assignment qic qif (@fapply variable function constructor f l)) *)
      unfold cache_left, cache_right, proj_left, proj_right in IHpi.
(* Goal: le (value_assignment qic v) (term_assignment qic qif (@fapply variable function constructor f l)) *)
      subst c2 l f0 v1.
(* Goal: le (value_assignment qic v) (term_assignment qic qif (@fapply variable function constructor f (@map (CBV_cache.cbv variable function constructor) (Syntax.term variable function constructor) (@proj_left variable function constructor) lp))) *)
      set (proof_tree:=cbv_update n v0 pi c (fapply f l0) c0 v).
(* Goal: le (suml (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) l0)) (suml (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l0)) *)
      subst l0.
(* Goal: le (value_assignment qic v) (term_assignment qic qif (@fapply variable function constructor f (@map (CBV_cache.cbv variable function constructor) (Syntax.term variable function constructor) (@proj_left variable function constructor) lp))) *)
      apply qi_right_le_qi_fapply_left with (proof_tree:=proof_tree) (c1:=c1);try tauto.
(* Goal: forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : cache_bounded qic qif (@cache_left variable function constructor p)) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p), and (le (value_assignment qic (@proj_right variable function constructor p)) (term_assignment qic qif (@proj_left variable function constructor p))) (cache_bounded qic qif (@cache_right variable function constructor p)) *)
      intros;apply H;trivial.
  + (* cbv_read *)
(* Goal: and (le (value_assignment qic v) (term_assignment qic qif (@fapply variable function constructor f l))) (cache_bounded qic qif c2) *)
    assert (cache_bounded qic qif c2).
    * (* preuve du assert *)
      destruct well_formed as (Hc2 & cpath &  Hl & Hl0 & wf_list & Hf & Hv & well_formed & arity).
(* Goal: cache_bounded qic qif c2 *)
      subst c2.
(* Goal: cache_bounded qic qif c *)
      apply cache_path_transitivity with (c:=c1) (c':=c) (l:=lp);auto.
(* Goal: forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : cache_bounded qic qif (@cache_left variable function constructor p)), cache_bounded qic qif (@cache_right variable function constructor p) *)
      intros;apply H;auto.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity a *)
      apply andl_in_map with (l:=lp);auto.
    * (* borne sur les QI *)
(* Goal: and (le (value_assignment qic v) (term_assignment qic qif t)) (cache_bounded qic qif c) *)
      split;auto.
      destruct well_formed as (Hc2 & cpath &  Hl & Hl0 & wf_list & Hf & Hv & well_formed & arity).
(* Goal: le (value_assignment qic v) (term_assignment qic qif (@fapply variable function constructor f l)) *)
      unfold cache_left in IHpi;unfold cache_right in IHpi.
(* Goal: le (value_assignment qic v) (term_assignment qic qif (@fapply variable function constructor f l)) *)
      subst c2 l f0 v0.
(* Goal: le (value_assignment qic v) (term_assignment qic qif (@fapply variable function constructor f (@map (CBV_cache.cbv variable function constructor) (Syntax.term variable function constructor) (@proj_left variable function constructor) lp))) *)
      set (proof_tree:=cbv_read c (fapply f l0) v).
(* Goal: le (suml (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) l0)) (suml (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l0)) *)
      subst l0.
(* Goal: le (value_assignment qic v) (term_assignment qic qif (@fapply variable function constructor f (@map (CBV_cache.cbv variable function constructor) (Syntax.term variable function constructor) (@proj_left variable function constructor) lp))) *)
      apply qi_right_le_qi_fapply_left with (proof_tree:=proof_tree) (c1:=c1);try tauto.
(* Goal: forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : cache_bounded qic qif (@cache_left variable function constructor p)) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p), and (le (value_assignment qic (@proj_right variable function constructor p)) (term_assignment qic qif (@proj_left variable function constructor p))) (cache_bounded qic qif (@cache_right variable function constructor p)) *)
      intros;apply H;trivial.
- (* cas cbv_update *)
(* Goal: and (le (value_assignment qic v) (term_assignment qic qif t)) (cache_bounded qic qif c2) *)
  assert (value_assignment qic v <= term_assignment qic qif t).
  + (* preuve du assert : borne sur les QI*)
(* Goal: le (value_assignment qic v) (term_assignment qic qif t) *)
    revert well_formed.
(* Goal: forall _ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity (@cbv_update variable function constructor n s pi c1 t c2 v), le (value_assignment qic v) (term_assignment qic qif t) *)
    elim t;simpl;try tauto.
(* Goal: forall _ : le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)))), le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (Datatypes.S O)) (qif f l)) (Datatypes.S O)) *)
    intros.
(* Goal: le (value_assignment qic v) (qif f (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l)) *)
    destruct well_formed as (_ & lp & r & length & rule & Hl & pl & pr & cl & _ & _ & wf_pi & _).
    rewrite cl in *;clear cl.
    rewrite pl in *;clear pl.
    rewrite pr in *;clear pr.
(* Goal: le (value_assignment qic v) (qif f (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l)) *)
    generalize (IHpi wf_pi cache).
(* Goal: forall _ : and (le (value_assignment qic v) (term_assignment qic qif (@subst variable function constructor s r))) (cache_bounded qic qif (@cache_right variable function constructor pi)), le (value_assignment qic v) (qif f (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l)) *)
    generalize (compat f lp r s).
(* Goal: forall _ : le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)))), le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (Datatypes.S O)) (qif f l)) (Datatypes.S O)) *)
    intros.
    replace (qif f (map (term_assignment qic qif) l)) with 
	    (term_assignment qic qif (subst s (lhs_of_rule (rule_intro f lp r)))).
    * apply le_trans with (m:=term_assignment qic qif (subst s r));try tauto.
(* Goal: le (term_assignment qic qif (@subst variable function constructor s r)) (term_assignment qic qif (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f lp r)))) *)
      apply H.
      rewrite <- rule;apply nth_In;auto.
(* Goal: @eq (option nat) (p_term_assignment qic qif (@Syntax.term_from_value variable function constructor (@c_capply constructor c l))) (@Some nat (value_assignment qic (@c_capply constructor c l))) *)
    * simpl.
(* Goal: @eq nat (qif f (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (@subst variable function constructor s) (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (@Syntax.term_from_pattern variable function constructor) lp)))) (qif f (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l)) *)
      rewrite Hl.
(* Goal: @eq nat (qif f (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (@subst variable function constructor s) (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (@Syntax.term_from_pattern variable function constructor) lp)))) (qif f (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp)))) *)
      rewrite (map_map (term_from_pattern) (subst s) lp).
(* Goal: @eq nat (qif f (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (fun x : Syntax.pattern variable constructor => @subst variable function constructor s (@Syntax.term_from_pattern variable function constructor x)) lp))) (qif f (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp)))) *)
      rewrite (map_map (psubst s) (term_from_value) lp).
(* Goal: @eq nat (qif f (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (fun x : Syntax.pattern variable constructor => @subst variable function constructor s (@Syntax.term_from_pattern variable function constructor x)) lp))) (qif f (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (fun x : Syntax.pattern variable constructor => @Syntax.term_from_value variable function constructor (@psubst variable constructor s x)) lp))) *)
      f_equal;f_equal.
(* Goal: @eq (list (Syntax.term variable function constructor)) (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (fun x : Syntax.pattern variable constructor => @subst variable function constructor s (@Syntax.term_from_pattern variable function constructor x)) lp) (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (fun x : Syntax.pattern variable constructor => @Syntax.term_from_value variable function constructor (@psubst variable constructor s x)) lp) *)
      clear.
(* Goal: @eq (list (Syntax.term variable function constructor)) (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (fun x : Syntax.pattern variable constructor => @subst variable function constructor s (@Syntax.term_from_pattern variable function constructor x)) lp) (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (fun x : Syntax.pattern variable constructor => @Syntax.term_from_value variable function constructor (@psubst variable constructor s x)) lp) *)
      induction lp as [ | p lp IH];simpl;trivial.
(* Goal: @eq (list (Syntax.term variable function constructor)) (@cons (Syntax.term variable function constructor) (@subst variable function constructor s (@Syntax.term_from_pattern variable function constructor p)) (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (fun x : Syntax.pattern variable constructor => @subst variable function constructor s (@Syntax.term_from_pattern variable function constructor x)) lp)) (@cons (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor (@psubst variable constructor s p)) (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (fun x : Syntax.pattern variable constructor => @Syntax.term_from_value variable function constructor (@psubst variable constructor s x)) lp)) *)
      rewrite IH.
(* Goal: @eq (list (Syntax.term variable function constructor)) (@cons (Syntax.term variable function constructor) (@subst variable function constructor s (@Syntax.term_from_pattern variable function constructor p)) (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (fun x : Syntax.pattern variable constructor => @Syntax.term_from_value variable function constructor (@psubst variable constructor s x)) lp)) (@cons (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor (@psubst variable constructor s p)) (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (fun x : Syntax.pattern variable constructor => @Syntax.term_from_value variable function constructor (@psubst variable constructor s x)) lp)) *)
      f_equal;apply subst_psubst.
 + (* preuve de la borne sur le cache *)
(* Goal: and (le (value_assignment qic v) (term_assignment qic qif t)) (cache_bounded qic qif c) *)
   split;auto.
(* Goal: le (term_assignment qic qif (@fapply variable function constructor f lv)) (qif f l) *)
   simpl in well_formed.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity pi *)
   destruct t;try tauto.
   destruct well_formed as (_ & _ & _ & _  & _ & _ & _ & _ & cl & _ & new_cache & wf_pi & _).
(* Goal: cache_bounded qic qif c2 *)
   subst c2.
(* Goal: cache_bounded qic qif (@cons (prod (Syntax.term variable function constructor) (Syntax.value constructor)) (@pair (Syntax.term variable function constructor) (Syntax.value constructor) (@fapply variable function constructor f l) v) (@cache_right variable function constructor pi)) *)
   unfold cache_bounded.
(* Goal: @Forall (prod (Syntax.term variable function constructor) (Syntax.value constructor)) (fun t : prod (Syntax.term variable function constructor) (Syntax.value constructor) => le (value_assignment qic (@snd (Syntax.term variable function constructor) (Syntax.value constructor) t)) (term_assignment qic qif (@fst (Syntax.term variable function constructor) (Syntax.value constructor) t))) (@cons (prod (Syntax.term variable function constructor) (Syntax.value constructor)) (@pair (Syntax.term variable function constructor) (Syntax.value constructor) (@fapply variable function constructor f l) v) (@cache_right variable function constructor pi)) *)
   apply Forall_cons.
   * unfold fst, snd;auto.
   * apply IHpi;auto.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
     rewrite cl;auto.
- (* cas cbv_read *)
(* Goal: and (le (value_assignment qic v) (term_assignment qic qif t)) (cache_bounded qic qif c) *)
  split;auto.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity pi *)
  simpl in well_formed;destruct t;try tauto.
(* Goal: le (value_assignment qic v) (term_assignment qic qif (@fapply variable function constructor f l)) *)
  destruct well_formed as (c_hit & lv'& Hl).
(* Goal: le (value_assignment qic v) (term_assignment qic qif (@fapply variable function constructor f l)) *)
  unfold cache_bounded in cache.
(* Goal: le (value_assignment qic v) (term_assignment qic qif (@fapply variable function constructor f l)) *)
  apply (Forall_In_l ((fapply f l),v) cache).
  apply (assoc_in (term_beq variable_eq_dec function_eq_dec constructor_eq_dec)
(* Goal: option_le (p_term_assignment qic f (@subst variable function constructor s t)) (p_term_assignment qic f (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f0 lp t)))) *)
         (fapply f l) c);auto.
(* Goal: forall a b : Syntax.term variable function constructor, iff (@eq bool (@term_beq variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec a b) true) (@eq (Syntax.term variable function constructor) a b) *)
  apply (term_beq_eq variable_eq_dec function_eq_dec constructor_eq_dec).
Qed.

(***********************************************************************************)
(*                                                                                 *)
(*             Bornes globales                                                     *)
(*                                                                                 *)
(***********************************************************************************)

(* Lemma 69 *)
Lemma QI_never_increase_global qic qif cs: forall pi proof_tree:cbv, 
  valid_QI qic qif cs -> wf proof_tree -> 
  cache_bounded qic qif (cache_left proof_tree) -> InCBV pi proof_tree -> 
  term_assignment qic qif (proj_left pi) <= term_assignment qic qif (proj_left proof_tree).
Proof.
(* Goal: forall (pi proof_tree : CBV_cache.cbv variable function constructor) (_ : valid_QI qic qif cs) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity proof_tree) (_ : cache_bounded qic qif (@cache_left variable function constructor proof_tree)) (_ : @InCBV variable function constructor pi proof_tree), cache_bounded qic qif (@cache_left variable function constructor pi) *)
intros pi proof_tree valid well_formed cache subtree.
(* Goal: let t := @fapply variable function constructor f lt in let l := @map (Syntax.term variable function constructor) nat (fun _ : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor t)) lt in forall _ : @eq (list (Syntax.term variable function constructor)) lt (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor) lval), le (term_assignment qic qif t) (qif f l) *)
unfold valid_QI in valid.
(* Goal: let t := @fapply variable function constructor f lt in let l := @map (Syntax.term variable function constructor) nat (fun _ : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor t)) lt in forall _ : @eq (list (Syntax.term variable function constructor)) lt (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor) lval), le (term_assignment qic qif t) (qif f l) *)
destruct valid as (additivity & max_cs & non_zero & sub & mono & compat).
(* On a parfois besoin de valid en entier (pour appliquer le lemme clé) et parfois de ses composants.
(* Goal: valid_QI qic qif cs *)
   Détruire valid cause plein de "unfold valid_QI;tauto." à chaque application du lemme clé.
   Est-ce qu'on peut dupliquer l'hypothèse pour pouvoir à la fois conserver l'ensemble
   et les composants et se passer de ces unfold ?                                                   *)
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
induction proof_tree using cbv_ind2.
- (* cbv_constr *)
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
  simpl in subtree;destruct subtree as [equal | strict].
  + (* égalité *)
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
    subst pi;trivial.
  + (* liste de sous arbres *)
(* Goal: le (term_assignment qic qif (@fapply variable function constructor f lv)) (qif f l) *)
    simpl in well_formed.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
    destruct t;destruct v;try tauto.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
    destruct well_formed as (cpath & Hc & Hl & Hl0 & wf_list & arity).
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
    rewrite orl_map in strict.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
    destruct strict as (x & inlist & intree).    
(* Goal: le (term_assignment qic qif (@proj_left variable function constructor pi)) (qif f (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l0)) *)
    apply le_trans with (m:=term_assignment qic qif (proj_left x)).
    * { apply H;trivial.
        - apply andl_in_map with (l:=lp);trivial.
        - apply cache_path_transitivity_left with (c:=c1) (c':=c2) (l:=lp);trivial.
(* Goal: forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : cache_bounded qic qif (@cache_left variable function constructor p)), cache_bounded qic qif (@cache_right variable function constructor p) *)
          intros;apply (left_bound_to_right_bound qic qif cs);trivial.
          + unfold valid_QI;tauto.
          + apply andl_in_map with (l:=lp);trivial.
      }
    * simpl;subst l.
(* Goal: @eq (option nat) match (fix option_list_map (A : Type) (l : list (option A)) {struct l} : option (list A) := match l with | nil => @Some (list A) (@nil A) | cons (Some h as o) t => @option_map (list A) (list A) (@cons A h) (option_list_map A t) | cons (None as o) t => @None (list A) end) nat (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic qif) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor) l)) with | Some a => @Some nat (qic c a) | None => @None nat end (@Some nat (qic c (@map (Syntax.value constructor) nat (value_assignment qic) l))) *)
      rewrite additivity;rewrite map_map.
(* Goal: le (term_assignment qic qif (@proj_left variable function constructor x)) (Init.Nat.add (suml (@map (CBV_cache.cbv variable function constructor) nat (fun x : CBV_cache.cbv variable function constructor => term_assignment qic qif (@proj_left variable function constructor x)) lp)) (cs c)) *)
      apply Plus.le_plus_trans.
(* Goal: le (term_assignment qic qif (@proj_left variable function constructor x)) (suml (@map (CBV_cache.cbv variable function constructor) nat (fun x : CBV_cache.cbv variable function constructor => term_assignment qic qif (@proj_left variable function constructor x)) lp)) *)
      apply in_le_suml.
(* Goal: @In nat (term_assignment qic qif (@proj_left variable function constructor x)) (@map (CBV_cache.cbv variable function constructor) nat (fun x : CBV_cache.cbv variable function constructor => term_assignment qic qif (@proj_left variable function constructor x)) lp) *)
      apply in_map with (f:=fun x0 => term_assignment qic qif (proj_left x0));trivial.
- (* cbv_split *)
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
  simpl in subtree;destruct subtree as [equal | [single | strict]].
  + (* égalité *)
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
    subst pi;trivial.
  + (* le sous arbre isolé *)
(* Goal: le (term_assignment qic qif (@fapply variable function constructor f lv)) (qif f l) *)
    simpl in well_formed.
    destruct proof_tree;destruct t0;destruct t;try tauto;intuition; 
    (* cet intuition fait aussi du travail dans IHproof_tree *)
             subst f0 c2;try subst v1;try subst v0.
    * (* cbv_update au dessus *)
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
      { simpl;simpl in cache;simpl in H8.
(* Goal: le (term_assignment qic qif (@proj_left variable function constructor pi)) (qif f (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l0)) *)
        simpl in single;destruct single as [equal | strict]. 
        (* les deux cas sont identiques. Peut-on factoriser la preuve ? *)
        - apply le_trans with (m:=qif f (map (term_assignment qic qif) l)).
          + apply H8;auto.
(* Goal: cache_bounded qic qif c *)
            apply cache_path_transitivity with (c:=c1) (c':=c) (l:=lp);trivial.
(* Goal: forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : cache_bounded qic qif (@cache_left variable function constructor p)), cache_bounded qic qif (@cache_right variable function constructor p) *)
            intros;apply (left_bound_to_right_bound qic qif cs);trivial.
            * unfold valid_QI;tauto.
            * apply andl_in_map with (l:=lp);trivial.
          + apply mono.
(* Goal: @Forall2 nat nat le (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l) (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l0) *)
            subst l l0.
(* Goal: @eq (option nat) match (fix option_list_map (A : Type) (l : list (option A)) {struct l} : option (list A) := match l with | nil => @Some (list A) (@nil A) | cons (Some h as o) t => @option_map (list A) (list A) (@cons A h) (option_list_map A t) | cons (None as o) t => @None (list A) end) nat (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic qif) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor) l)) with | Some a => @Some nat (qic c a) | None => @None nat end (@Some nat (qic c (@map (Syntax.value constructor) nat (value_assignment qic) l))) *)
            rewrite map_map;rewrite map_map;rewrite map_map.
(* Goal: @Forall2 nat nat le (@map (Syntax.term variable function constructor) nat (fun v : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor v)) lt) (@map (Syntax.term variable function constructor) nat (fun _ : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor t)) lt) *)
            apply Forall2_map.
(* Goal: forall _ : le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)))), le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (Datatypes.S O)) (qif f l)) (Datatypes.S O)) *)
            intros.
            apply le_trans with (m:=value_assignment qic (proj_right x)). (* coercion de type *)
            * apply Nat.eq_le_incl.
(* Goal: @eq nat (term_assignment qic qif (@Syntax.term_from_value variable function constructor (@proj_right variable function constructor x))) (value_assignment qic (@proj_right variable function constructor x)) *)
              apply value_as_term_assignment.
            * apply (left_bound_to_right_bound qic qif cs);trivial.
(* Goal: valid_QI qic qif cs *)
              unfold valid_QI;tauto.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p *)
              apply andl_in_map with (l:=lp);trivial.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor x) *)
              apply cache_path_transitivity_left with (c:=c1) (c':=c) (l:=lp);trivial.
(* Goal: forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : cache_bounded qic qif (@cache_left variable function constructor p)), cache_bounded qic qif (@cache_right variable function constructor p) *)
              intros;apply (left_bound_to_right_bound qic qif cs);trivial.
(* Goal: valid_QI qic qif cs *)
              unfold valid_QI;tauto.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p *)
              apply andl_in_map with (l:=lp);trivial.
        - apply le_trans with (m:=qif f (map (term_assignment qic qif) l)).
          + apply H8;auto.
(* Goal: cache_bounded qic qif c *)
            apply cache_path_transitivity with (c:=c1) (c':=c) (l:=lp);trivial.
(* Goal: forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : cache_bounded qic qif (@cache_left variable function constructor p)), cache_bounded qic qif (@cache_right variable function constructor p) *)
            intros;apply (left_bound_to_right_bound qic qif cs);trivial.
            * unfold valid_QI;tauto.
            * apply andl_in_map with (l:=lp);trivial.
          + apply mono.
(* Goal: @Forall2 nat nat le (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l) (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l0) *)
            subst l l0.
(* Goal: @eq (option nat) match (fix option_list_map (A : Type) (l : list (option A)) {struct l} : option (list A) := match l with | nil => @Some (list A) (@nil A) | cons (Some h as o) t => @option_map (list A) (list A) (@cons A h) (option_list_map A t) | cons (None as o) t => @None (list A) end) nat (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic qif) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor) l)) with | Some a => @Some nat (qic c a) | None => @None nat end (@Some nat (qic c (@map (Syntax.value constructor) nat (value_assignment qic) l))) *)
            rewrite map_map;rewrite map_map;rewrite map_map.
(* Goal: @Forall2 nat nat le (@map (Syntax.term variable function constructor) nat (fun v : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor v)) lt) (@map (Syntax.term variable function constructor) nat (fun _ : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor t)) lt) *)
            apply Forall2_map.
(* Goal: forall _ : le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)))), le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (Datatypes.S O)) (qif f l)) (Datatypes.S O)) *)
            intros.
(* Goal: le (term_assignment qic qif (@Syntax.term_from_value variable function constructor (@proj_right variable function constructor x))) (term_assignment qic qif (@proj_left variable function constructor x)) *)
            apply le_trans with (m:=value_assignment qic (proj_right x)).
            * apply Nat.eq_le_incl.
(* Goal: @eq nat (term_assignment qic qif (@Syntax.term_from_value variable function constructor (@proj_right variable function constructor x))) (value_assignment qic (@proj_right variable function constructor x)) *)
              apply value_as_term_assignment.
            * apply (left_bound_to_right_bound qic qif cs);trivial.
(* Goal: valid_QI qic qif cs *)
              unfold valid_QI;tauto.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p *)
              apply andl_in_map with (l:=lp);trivial.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor x) *)
              apply cache_path_transitivity_left with (c:=c1) (c':=c) (l:=lp);trivial.
(* Goal: forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : cache_bounded qic qif (@cache_left variable function constructor p)), cache_bounded qic qif (@cache_right variable function constructor p) *)
              intros;apply (left_bound_to_right_bound qic qif cs);trivial.
(* Goal: valid_QI qic qif cs *)
              unfold valid_QI;tauto.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p *)
              apply andl_in_map with (l:=lp);trivial.
      }
    * (* cbv_read au dessus *)
(* Goal: le (term_assignment qic qif (@proj_left variable function constructor pi)) (term_assignment qic qif (@proj_left variable function constructor (@cbv_split variable function constructor lp (@cbv_read variable function constructor c (@fapply variable function constructor f l) v) c1 (@fapply variable function constructor f l0) c v))) *)
      simpl in cache;simpl in single;simpl in H8.
(* Goal: le (term_assignment qic qif (@proj_left variable function constructor pi)) (term_assignment qic qif (@proj_left variable function constructor (@cbv_split variable function constructor lp (@cbv_read variable function constructor c (@fapply variable function constructor f l) v) c1 (@fapply variable function constructor f l0) c v))) *)
      destruct single as [equal | false];try tauto.
      subst pi;simpl in *.
(* Goal: le (qif f (@map (Syntax.term variable function constructor) nat (fun v : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor v)) lt)) (qif f (@map (Syntax.term variable function constructor) nat (fun _ : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor t)) lt)) *)
      apply mono.
(* Goal: @Forall2 nat nat le (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l) (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l0) *)
      subst l l0.
(* Goal: @eq (option nat) match (fix option_list_map (A : Type) (l : list (option A)) {struct l} : option (list A) := match l with | nil => @Some (list A) (@nil A) | cons (Some h as o) t => @option_map (list A) (list A) (@cons A h) (option_list_map A t) | cons (None as o) t => @None (list A) end) nat (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic qif) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor) l)) with | Some a => @Some nat (qic c a) | None => @None nat end (@Some nat (qic c (@map (Syntax.value constructor) nat (value_assignment qic) l))) *)
      rewrite map_map;rewrite map_map;rewrite map_map.
(* Goal: @Forall2 nat nat le (@map (Syntax.term variable function constructor) nat (fun v : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor v)) lt) (@map (Syntax.term variable function constructor) nat (fun _ : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor t)) lt) *)
      apply Forall2_map.
(* Goal: forall _ : le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)))), le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (Datatypes.S O)) (qif f l)) (Datatypes.S O)) *)
      intros.
      { apply le_trans with (m:=value_assignment qic (proj_right x)).  (* coercion de type *)
        - apply Nat.eq_le_incl.
(* Goal: @eq nat (term_assignment qic qif (@Syntax.term_from_value variable function constructor (@proj_right variable function constructor x))) (value_assignment qic (@proj_right variable function constructor x)) *)
          apply value_as_term_assignment.
        - apply (left_bound_to_right_bound qic qif cs);trivial.
          + unfold valid_QI;tauto.
          + apply andl_in_map with (l:=lp);trivial.
          + apply cache_path_transitivity_left with (c:=c1) (c':=c) (l:=lp);trivial.
(* Goal: forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : cache_bounded qic qif (@cache_left variable function constructor p)), cache_bounded qic qif (@cache_right variable function constructor p) *)
            intros;apply (left_bound_to_right_bound qic qif cs);trivial.
            * unfold valid_QI;tauto.
            * apply andl_in_map with (l:=lp);trivial.
      }
  + (* liste de sous arbres *)
(* Goal: le (term_assignment qic qif (@fapply variable function constructor f lv)) (qif f l) *)
    simpl in well_formed.
    destruct proof_tree;destruct t0;destruct t;try tauto;intuition;
    (* cet intuition fait aussi du travail dans IHproof_tree *)
             simpl;simpl in H9;simpl in cache;subst c2 f0;try subst v1;try subst v0.
    (* les deux cas sont identiques, peut-on factoriser ? *)
    * (* cbv_update au dessus *)
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
      { rewrite orl_map in strict.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
        destruct strict as (x & inlist & intree).
(* Goal: le (term_assignment qic qif (@proj_left variable function constructor pi)) (qif f (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l0)) *)
        apply le_trans with (m:=term_assignment qic qif (proj_left x)).
        - apply H;trivial.
          + apply andl_in_map with (l:=lp);trivial.
          + apply cache_path_transitivity_left with (c:=c1) (c':=c) (l:=lp);trivial.
(* Goal: forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : cache_bounded qic qif (@cache_left variable function constructor p)), cache_bounded qic qif (@cache_right variable function constructor p) *)
            intros;apply (left_bound_to_right_bound qic qif cs);trivial.
            * unfold valid_QI;tauto.
            * apply andl_in_map with (l:=lp);trivial.
        - subst l0;rewrite map_map.
(* Goal: le (term_assignment qic qif (@proj_left variable function constructor x)) (qif f (@map (CBV_cache.cbv variable function constructor) nat (fun x : CBV_cache.cbv variable function constructor => term_assignment qic qif (@proj_left variable function constructor x)) lp)) *)
          apply sub.
(* Goal: @In nat (term_assignment qic qif (@proj_left variable function constructor x)) (@map (CBV_cache.cbv variable function constructor) nat (fun x : CBV_cache.cbv variable function constructor => term_assignment qic qif (@proj_left variable function constructor x)) lp) *)
          apply in_map with (f:=fun x0 => term_assignment qic qif (proj_left x0));trivial.
      }
    * (* cbv_read au dessus *)
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
      { rewrite orl_map in strict.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
        destruct strict as (x & inlist & intree).
(* Goal: le (term_assignment qic qif (@proj_left variable function constructor pi)) (qif f (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l0)) *)
        apply le_trans with (m:=term_assignment qic qif (proj_left x)).
        - apply H;trivial.
          + apply andl_in_map with (l:=lp);trivial.
          + apply cache_path_transitivity_left with (c:=c1) (c':=c) (l:=lp);trivial.
(* Goal: forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : cache_bounded qic qif (@cache_left variable function constructor p)), cache_bounded qic qif (@cache_right variable function constructor p) *)
            intros;apply (left_bound_to_right_bound qic qif cs);trivial.
            * unfold valid_QI;tauto.
            * apply andl_in_map with (l:=lp);trivial.
        - subst l0;rewrite map_map.
(* Goal: le (term_assignment qic qif (@proj_left variable function constructor x)) (qif f (@map (CBV_cache.cbv variable function constructor) nat (fun x : CBV_cache.cbv variable function constructor => term_assignment qic qif (@proj_left variable function constructor x)) lp)) *)
          apply sub.
(* Goal: @In nat (term_assignment qic qif (@proj_left variable function constructor x)) (@map (CBV_cache.cbv variable function constructor) nat (fun x : CBV_cache.cbv variable function constructor => term_assignment qic qif (@proj_left variable function constructor x)) lp) *)
          apply in_map with (f:=fun x0 => term_assignment qic qif (proj_left x0));trivial.
      }
- (* cbv_update *)
(* Goal: le (term_assignment qic qif (@proj_left variable function constructor pi)) (term_assignment qic qif (@proj_left variable function constructor (@cbv_update variable function constructor n s proof_tree c1 t c2 v))) *)
  simpl;simpl in cache.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
  simpl in subtree;destruct subtree as [equal | strict].
  + (* égalité *)
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
    subst pi;trivial.
  + (* sous arbre *)
(* Goal: le (term_assignment qic qif (@fapply variable function constructor f lv)) (qif f l) *)
    simpl in well_formed.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity pi *)
    destruct t;try tauto.
(* Goal: le (term_assignment qic qif (@proj_left variable function constructor pi)) (term_assignment qic qif (@fapply variable function constructor f l)) *)
    destruct well_formed as (_ & lp & t & n_le_lp & rule & Hl & pl & pr & cl & _ & _ & wf_ind & _).
(* Goal: le (term_assignment qic qif (@proj_left variable function constructor pi)) (term_assignment qic qif (@fapply variable function constructor f l)) *)
    apply le_trans with (m:=term_assignment qic qif (proj_left proof_tree)).
    * subst c1;apply IHproof_tree;trivial.
    * rewrite pl.
(* Goal: le (term_assignment qic qif (@subst variable function constructor s t)) (term_assignment qic qif (@fapply variable function constructor f l)) *)
      simpl;unfold compatible_QI in compat.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
      { replace l with (map (subst s) (map term_from_pattern lp)).
        - apply compat.
          rewrite <- rule;apply nth_In;trivial.
        - subst l.
(* Goal: @eq (option nat) match (fix option_list_map (A : Type) (l : list (option A)) {struct l} : option (list A) := match l with | nil => @Some (list A) (@nil A) | cons (Some h as o) t => @option_map (list A) (list A) (@cons A h) (option_list_map A t) | cons (None as o) t => @None (list A) end) nat (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic qif) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor) l)) with | Some a => @Some nat (qic c a) | None => @None nat end (@Some nat (qic c (@map (Syntax.value constructor) nat (value_assignment qic) l))) *)
          rewrite map_map;rewrite map_map.
(* Goal: @eq (list (Syntax.term variable function constructor)) (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (fun x : Syntax.pattern variable constructor => @subst variable function constructor s (@Syntax.term_from_pattern variable function constructor x)) lp) (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (fun x : Syntax.pattern variable constructor => @Syntax.term_from_value variable function constructor (@psubst variable constructor s x)) lp) *)
          apply map_ext.
(* Goal: forall a : Syntax.pattern variable constructor, @eq (Syntax.term variable function constructor) (@subst variable function constructor s (@Syntax.term_from_pattern variable function constructor a)) (@Syntax.term_from_value variable function constructor (@psubst variable constructor s a)) *)
          intros;apply subst_psubst.
      }
- (* cbv_read *)
(* Goal: le (term_assignment qic qif (@proj_left variable function constructor pi)) (term_assignment qic qif (@proj_left variable function constructor (@cbv_read variable function constructor c t v))) *)
  simpl in subtree;destruct subtree as [equal | impossible];try tauto.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
  subst pi;trivial.
Qed.

Lemma cache_left_bounded_global qic qif cs: forall pi proof_tree:cbv,
  valid_QI qic qif cs -> wf proof_tree -> 
  cache_bounded qic qif (cache_left proof_tree) -> InCBV pi proof_tree ->
  cache_bounded qic qif (cache_left pi).
Proof.
(* Goal: forall (pi proof_tree : CBV_cache.cbv variable function constructor) (_ : valid_QI qic qif cs) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity proof_tree) (_ : cache_bounded qic qif (@cache_left variable function constructor proof_tree)) (_ : @InCBV variable function constructor pi proof_tree), cache_bounded qic qif (@cache_left variable function constructor pi) *)
intros pi proof_tree valid well_formed cache subtree.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
induction proof_tree using cbv_ind2.
- (* cbv_constr *)
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
  simpl in subtree;destruct subtree as [ equal | strict].
  + (* égalité *)
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
    subst pi;trivial.
  + (* liste de sous arbres *)
(* Goal: le (term_assignment qic qif (@fapply variable function constructor f lv)) (qif f l) *)
    simpl in well_formed.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
    destruct t;destruct v;try tauto.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
    destruct well_formed as (cpath & Hc & Hl & Hl0 & wf_list & arity).
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
    rewrite orl_map in strict.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
    destruct strict as (x & inlist & intree).
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
    apply H with (p:=x);auto.
    * apply andl_in_map with (l:=lp);trivial.
    * apply cache_path_transitivity_left with (c:=c1) (c':=c2) (l:=lp);auto.
(* Goal: forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : cache_bounded qic qif (@cache_left variable function constructor p)), cache_bounded qic qif (@cache_right variable function constructor p) *)
      intros;apply (left_bound_to_right_bound qic qif cs);trivial.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p *)
      apply andl_in_map with (l:=lp);trivial.
- (* cbv_split *)
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
  simpl in subtree;destruct subtree as [equal | [single | strict]].
  + (* égalité *)
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
    subst pi;trivial.
  + (* le sous arbre isolé *)
(* Goal: le (term_assignment qic qif (@fapply variable function constructor f lv)) (qif f l) *)
    simpl in well_formed.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
    destruct proof_tree;destruct t0;destruct t;try tauto;intuition;simpl in cache.
    (* cet intuition fait aussi du travail dans IHproof_tree *)
    * (* cbv_update au dessus *)
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
      apply H8;auto.
(* Goal: @eq (option nat) (p_term_assignment qic qif (@Syntax.term_from_value variable function constructor (@c_capply constructor c l))) (@Some nat (value_assignment qic (@c_capply constructor c l))) *)
      simpl.
(* Goal: cache_bounded qic qif c *)
      apply cache_path_transitivity with (c:=c1) (l:=lp);auto.
(* Goal: forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : cache_bounded qic qif (@cache_left variable function constructor p)), cache_bounded qic qif (@cache_right variable function constructor p) *)
      intros;apply (left_bound_to_right_bound qic qif cs);trivial.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p *)
      apply andl_in_map with (l:=lp);trivial.
    * (* cbv_read au dessus *)
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
      simpl in single;destruct single as [equal | impossible];try tauto.
(* Goal: @eq (option nat) (p_term_assignment qic qif (@Syntax.term_from_value variable function constructor (@c_capply constructor c l))) (@Some nat (value_assignment qic (@c_capply constructor c l))) *)
      subst pi;simpl.
(* Goal: cache_bounded qic qif c *)
      apply cache_path_transitivity with (c:=c1) (c':=c) (l:=lp);auto.
(* Goal: forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : cache_bounded qic qif (@cache_left variable function constructor p)), cache_bounded qic qif (@cache_right variable function constructor p) *)
      intros;apply (left_bound_to_right_bound qic qif cs);trivial.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p *)
      apply andl_in_map with (l:=lp);trivial.
  + (* liste de sous arbres *)
(* Goal: le (term_assignment qic qif (@fapply variable function constructor f lv)) (qif f l) *)
    simpl in well_formed.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
    destruct proof_tree;destruct t0;destruct t;try tauto;intuition.
    (* cet intuition fait aussi du travail dans IHproof_tree *)
    (* les deux cas sont identiques, peut-on factoriser ? *)
    * (* cbv_update au dessus *)
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
      { rewrite orl_map in strict.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
        destruct strict as (x & inlist & intree).
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
        apply H with (p:=x);auto.
        - apply andl_in_map with (l:=lp);trivial.
        - apply cache_path_transitivity_left with (c:=c1) (c':=c) (l:=lp);auto.
(* Goal: forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : cache_bounded qic qif (@cache_left variable function constructor p)), cache_bounded qic qif (@cache_right variable function constructor p) *)
          intros;apply (left_bound_to_right_bound qic qif cs);trivial.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p *)
          apply andl_in_map with (l:=lp);trivial.
      }
    * (* cbv_read au dessus *)
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
      { rewrite orl_map in strict.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
        destruct strict as (x & inlist & intree).
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
        apply H with (p:=x);auto.
        - apply andl_in_map with (l:=lp);trivial.
        - apply cache_path_transitivity_left with (c:=c1) (c':=c) (l:=lp);auto.
(* Goal: forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : cache_bounded qic qif (@cache_left variable function constructor p)), cache_bounded qic qif (@cache_right variable function constructor p) *)
          intros;apply (left_bound_to_right_bound qic qif cs);trivial.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p *)
          apply andl_in_map with (l:=lp);trivial.
      }
- (* cbv_update *)
(* Goal: le (term_assignment qic qif (@fapply variable function constructor f lv)) (qif f l) *)
  simpl in well_formed.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity pi *)
  destruct t;try tauto.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
  simpl in cache.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
  destruct well_formed as (_ & _ & _ & _ & _ & _ & _ & _ & cl & _ & _ & wf_ind & _).
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
  simpl in subtree.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
  destruct subtree as [equal | strict].
  + subst pi;simpl;tauto.
  + apply IHproof_tree;auto.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor proof_tree) *)
    rewrite cl;trivial.   
- (* cbv_read *)
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
  simpl in subtree.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
  destruct subtree as [equal | impossible];try tauto.
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
  subst pi;simpl;trivial.
Qed.

Definition judgsize (p:cbv) := term_size (proj_left p) + value_size (proj_right p).

(* remarque préliminaire du Théorème 70 *)
Lemma qi_active_bounded_by_size qic qif cs: forall f lval lt,
  valid_QI qic qif cs ->
  let t :=  (fapply f lt) in
  let l := (map (fun x=> mcs * (term_size t)) lt) in
  (* lt devrait aussi être défini par un let … in, mais ça plante à l'application du lemme et
     je ne comprends pas pourquoi. *)
  lt = map term_from_value lval ->
  term_assignment qic qif t <= (qif f l).
Proof.
(* Goal: forall (f : function) (lval : list (Syntax.value constructor)) (lt : list (Syntax.term variable function constructor)) (_ : valid_QI qic qif cs), let t := @fapply variable function constructor f lt in let l := @map (Syntax.term variable function constructor) nat (fun _ : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor t)) lt in forall _ : @eq (list (Syntax.term variable function constructor)) lt (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor) lval), le (term_assignment qic qif t) (qif f l) *)
intros f lval lt valid.
(* Goal: let t := @fapply variable function constructor f lt in let l := @map (Syntax.term variable function constructor) nat (fun _ : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor t)) lt in forall _ : @eq (list (Syntax.term variable function constructor)) lt (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor) lval), le (term_assignment qic qif t) (qif f l) *)
unfold valid_QI in valid.
(* Goal: let t := @fapply variable function constructor f lt in let l := @map (Syntax.term variable function constructor) nat (fun _ : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor t)) lt in forall _ : @eq (list (Syntax.term variable function constructor)) lt (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor) lval), le (term_assignment qic qif t) (qif f l) *)
destruct valid as (additivity & max_cs & non_zero & sub & mono & compat).
(* Goal: forall _ : le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)))), le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (Datatypes.S O)) (qif f l)) (Datatypes.S O)) *)
intros.
apply le_trans with (m:=qif f (map (fun v => mcs*(term_size v)) lt)).
(* Goal: le (term_assignment qic qif t) (qif f (@map (Syntax.term variable function constructor) nat (fun v : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor v)) lt)) *)
(* Goal: le (qif f (@map (Syntax.term variable function constructor) nat (fun v : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor v)) lt)) (qif f l) *)
apply le_trans with (m:=qif f (map (term_assignment qic qif) lt)).
- simpl;auto.
- apply mono.
(* Goal: @Forall2 nat nat le (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) lt) (@map (Syntax.term variable function constructor) nat (fun v : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor v)) lt) *)
  subst lt.
(* Goal: @eq (option nat) match (fix option_list_map (A : Type) (l : list (option A)) {struct l} : option (list A) := match l with | nil => @Some (list A) (@nil A) | cons (Some h as o) t => @option_map (list A) (list A) (@cons A h) (option_list_map A t) | cons (None as o) t => @None (list A) end) nat (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic qif) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor) l)) with | Some a => @Some nat (qic c a) | None => @None nat end (@Some nat (qic c (@map (Syntax.value constructor) nat (value_assignment qic) l))) *)
  rewrite map_map;rewrite map_map.
(* Goal: @Forall2 nat nat le (@map (Syntax.term variable function constructor) nat (fun v : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor v)) lt) (@map (Syntax.term variable function constructor) nat (fun _ : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor t)) lt) *)
  apply Forall2_map.
(* Goal: forall _ : le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)))), le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (Datatypes.S O)) (qif f l)) (Datatypes.S O)) *)
  intros.
(* Goal: le (@term_size variable function constructor (@Syntax.term_from_value variable function constructor x0)) (term_assignment qic qif (@Syntax.term_from_value variable function constructor x0)) *)
  rewrite compatible_sizes.
(* Goal: le (@value_size constructor x0) (term_assignment qic qif (@Syntax.term_from_value variable function constructor x0)) *)
  rewrite value_as_term_assignment.
(* Goal: le (value_assignment qic x) (Init.Nat.mul mcs (@value_size constructor x)) *)
  apply (QI_le_value_size qic cs);trivial.
- unfold l.
(* Goal: le (qif f (@map (Syntax.term variable function constructor) nat (fun v : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor v)) lt)) (qif f (@map (Syntax.term variable function constructor) nat (fun _ : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor t)) lt)) *)
  apply mono.
  
(* Goal: @Forall2 nat nat le (@map (Syntax.term variable function constructor) nat (fun v : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor v)) lt) (@map (Syntax.term variable function constructor) nat (fun _ : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor t)) lt) *)
  apply Forall2_map.
(* Goal: forall _ : le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)))), le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (Datatypes.S O)) (qif f l)) (Datatypes.S O)) *)
  intros.
(* Goal: le (Init.Nat.mul mcs (@term_size variable function constructor x)) (Init.Nat.mul mcs (@term_size variable function constructor t)) *)
  apply Mult.mult_le_compat_l.
(* Goal: @eq (option nat) (p_term_assignment qic qif (@Syntax.term_from_value variable function constructor (@c_capply constructor c l))) (@Some nat (value_assignment qic (@c_capply constructor c l))) *)
  simpl.
(* Goal: le (@term_size variable function constructor x) (S (suml (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) lt))) *)
  apply le_trans with (m:=suml (map (term_size (constructor:=constructor)) lt)).
(* Goal: le (@term_size variable function constructor x) (suml (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) lt)) *)
(* Goal: le (suml (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) lt)) (S (suml (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) lt))) *)
  apply le_trans with (m:=maxl (map (term_size (constructor:=constructor)) lt)).
  + apply maxl_is_max.
(* Goal: @In nat (term_assignment qic qif x) (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l0) *)
    apply in_map;trivial.
  + apply maxl_le_suml.
  + omega. 
Qed.

(* Théorème 70 *)
Lemma active_size_bound qic qif cs: forall i sub p c f lv d v, forall pi,
  valid_QI qic qif cs ->
  let t :=  (fapply f lv) in
  let proof_tree := cbv_update i sub p c t d v in 
  let l:= (map (fun x=> mcs * (term_size t)) lv) in
  wf proof_tree -> In pi (activations proof_tree) -> cache_bounded qic qif c -> 
  judgsize pi <= (max_arity + 1) * (qif f l) + 1.
Proof.
(* Goal: forall (i : nat) (sub : forall _ : variable, Syntax.value constructor) (p : CBV_cache.cbv variable function constructor) (c : CBV_cache.cache variable function constructor) (f : function) (lv : list (Syntax.term variable function constructor)) (d : CBV_cache.cache variable function constructor) (v : Syntax.value constructor) (pi : CBV_cache.cbv variable function constructor) (_ : valid_QI qic qif cs), let t := @fapply variable function constructor f lv in let proof_tree := @cbv_update variable function constructor i sub p c t d v in let l := @map (Syntax.term variable function constructor) nat (fun _ : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor t)) lv in forall (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity proof_tree) (_ : @In (CBV_cache.cbv variable function constructor) pi (@activations variable function constructor proof_tree)) (_ : cache_bounded qic qif c), le (judgsize pi) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (S O)) (qif f l)) (S O)) *)
intros i sub p c f lv d v pi valid t proof_tree l well_formed active cache.
(* Goal: le (judgsize pi) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (S O)) (qif f l)) (S O)) *)
unfold valid_QI in valid;destruct valid as (additivity & max_cs & non_zero & subt & mono & compat).
(* pour ajouter les hypothèses explicitement *)
(* Goal: le (judgsize pi) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (S O)) (qif f l)) (S O)) *)
assert (InCBV pi proof_tree) as subtree.
(* Goal: @InCBV variable function constructor pi proof_tree *)
(* Goal: le (judgsize pi) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (S O)) (qif f l)) (S O)) *)
apply activations_inCBV;trivial.
(* Goal: le (judgsize pi) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (S O)) (qif f l)) (S O)) *)
assert (wf pi) as sub_wf.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity (@cbv_update variable function constructor n v1 pi c0 s c3 u) *)
apply wf_InCBV_wf with (proof_tree:=proof_tree);trivial.
(* maintenant, on peut détruire active pour forcer la forme de pi *)
(* Goal: le (judgsize pi) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (S O)) (qif f l)) (S O)) *)
apply activation_is_function in active.
(* Goal: le (judgsize pi) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (S O)) (qif f l)) (S O)) *)
destruct active as (i' & sub' & p' & c1 & t0 & c2 & v0 & pi_is_upd).
(* Goal: le (judgsize pi) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (S O)) (qif f l)) (S O)) *)
destruct pi;try discriminate pi_is_upd.
(* Goal: @eq (option nat) (p_term_assignment qic qif (@Syntax.term_from_value variable function constructor (@c_capply constructor c l))) (@Some nat (value_assignment qic (@c_capply constructor c l))) *)
simpl.
(* Goal: le (judgsize (@cbv_update variable function constructor n v1 pi c0 t1 c3 v2)) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (S O)) (qif f l)) (S O)) *)
simpl in sub_wf;destruct t1;try tauto.
(* Goal: le (judgsize (@cbv_update variable function constructor n v1 pi c0 (@fapply variable function constructor f0 l0) c3 v2)) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (S O)) (qif f l)) (S O)) *)
destruct sub_wf as (_ & lp & _ & _ & _ & Hl0 & _ & _ & _ & _ & _ & _ & arity).
(* Goal: le (judgsize (@cbv_update variable function constructor n v1 pi c0 (@fapply variable function constructor f0 l0) c3 v2)) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (S O)) (qif f l)) (S O)) *)
set (s:=fapply f0 l0);set (u:=v2).

(* On empile les inégalités *)
apply le_trans with (m:=(max_arity+1) * (term_assignment qic qif (fapply f lv)) + 1).
apply le_trans with (m:=(max_arity+1)*(term_assignment qic qif s) + 1).
apply le_trans with (m:=(length l0)*(term_assignment qic qif s) + (term_assignment qic qif s) + 1).
apply le_trans with (m:=suml (map (fun t => term_assignment qic qif s) l0) + (term_assignment qic qif s) + 1).
apply le_trans with (m:=suml (map (term_assignment qic qif) l0) + (term_assignment qic qif s) + 1).
apply le_trans with (m:=suml (map (@term_size _ _ _) l0) + (term_assignment qic qif s) + 1).
apply le_trans with (m:=(term_size s) + (term_assignment qic qif s)).
apply le_trans with (m:=(term_size s) + (value_assignment qic u)).
apply le_trans with (m:=(term_size s) + (value_size u)).

(* Et on les dépile *)
- auto.
- apply Plus.plus_le_compat_l.
(* Goal: option_le (p_term_assignment qic f (@subst variable function constructor s t)) (p_term_assignment qic f (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f0 lp t)))) *)
  apply (value_size_le_QI qic cs);auto.
- apply Plus.plus_le_compat_l.
  apply (left_bound_to_right_bound qic qif cs) with (pi:=cbv_update n v1 pi c0 s c3 u);trivial. (* lemme clé *)
  + unfold valid_QI;tauto.
  + apply wf_InCBV_wf with (proof_tree:=proof_tree);trivial.
  + apply (cache_left_bounded_global qic qif cs) with (proof_tree:=proof_tree);auto.
(* Goal: valid_QI qic qif cs *)
    unfold valid_QI;tauto.
- simpl;omega.
- apply Plus.plus_le_compat_r;apply Plus.plus_le_compat_r.
(* Goal: le (suml (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) l0)) (suml (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l0)) *)
  subst l0.
(* Goal: forall _ : le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)))), le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (Datatypes.S O)) (qif f l)) (Datatypes.S O)) *)
  apply suml_map_le;intros.
(* Goal: le (@term_size variable function constructor x) (term_assignment qic qif x) *)
  rewrite in_map_iff in H;destruct H;destruct H as (eq & inl).
(* Goal: le (@term_size variable function constructor x) (term_assignment qic qif x) *)
  subst x.
(* Goal: le (@term_size variable function constructor (@Syntax.term_from_value variable function constructor x0)) (term_assignment qic qif (@Syntax.term_from_value variable function constructor x0)) *)
  rewrite compatible_sizes.
(* Goal: le (@value_size constructor x0) (term_assignment qic qif (@Syntax.term_from_value variable function constructor x0)) *)
  rewrite value_as_term_assignment.
(* Goal: le (@value_size constructor x0) (value_assignment qic x0) *)
  apply (value_size_le_QI qic cs);trivial.
- apply Plus.plus_le_compat_r;apply Plus.plus_le_compat_r.
(* Goal: forall _ : le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)))), le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (Datatypes.S O)) (qif f l)) (Datatypes.S O)) *)
  apply suml_map_le;intros.
(* Goal: @eq (option nat) (p_term_assignment qic qif (@Syntax.term_from_value variable function constructor (@c_capply constructor c l))) (@Some nat (value_assignment qic (@c_capply constructor c l))) *)
  unfold s;simpl.
(* Goal: le (term_assignment qic qif x) (qif f0 (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l0)) *)
  apply subt.
(* Goal: @In nat (term_assignment qic qif x) (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) l0) *)
  apply in_map;trivial.
- apply Plus.plus_le_compat_r;apply Plus.plus_le_compat_r.
(* Goal: le (suml (@map (Syntax.term variable function constructor) nat (fun _ : Syntax.term variable function constructor => term_assignment qic qif s) l0)) (Init.Nat.mul (@length (Syntax.term variable function constructor) l0) (term_assignment qic qif s)) *)
  rewrite Mult.mult_comm.
(* Goal: le (suml (@map (Syntax.term variable function constructor) nat (fun _ : Syntax.term variable function constructor => term_assignment qic qif s) l0)) (Nat.mul (term_assignment qic qif s) (@length (Syntax.term variable function constructor) l0)) *)
  apply Nat.eq_le_incl.
(* Goal: @eq nat (suml (@map (Syntax.term variable function constructor) nat (fun _ : Syntax.term variable function constructor => term_assignment qic qif s) l0)) (Nat.mul (term_assignment qic qif s) (@length (Syntax.term variable function constructor) l0)) *)
  apply suml_map_const.
- apply Plus.plus_le_compat_r.
(* Goal: le (Init.Nat.add (Init.Nat.mul (@length (Syntax.term variable function constructor) l0) (term_assignment qic qif s)) (term_assignment qic qif s)) (Init.Nat.mul (Init.Nat.add max_arity (S O)) (term_assignment qic qif s)) *)
  rewrite Mult.mult_plus_distr_r.
(* Goal: le (Init.Nat.add (Init.Nat.mul (@length (Syntax.term variable function constructor) l0) (term_assignment qic qif s)) (term_assignment qic qif s)) (Nat.add (Nat.mul max_arity (term_assignment qic qif s)) (Nat.mul (S O) (term_assignment qic qif s))) *)
  rewrite Mult.mult_1_l.
(* Goal: le (Init.Nat.add (Init.Nat.mul (@length (Syntax.term variable function constructor) l0) (term_assignment qic qif s)) (term_assignment qic qif s)) (Nat.add (Nat.mul max_arity (term_assignment qic qif s)) (term_assignment qic qif s)) *)
  apply Plus.plus_le_compat_r;apply Mult.mult_le_compat_r;trivial.
- apply Plus.plus_le_compat_r;apply Mult.mult_le_compat_l.
  apply (QI_never_increase_global qic qif cs) with 
(* Goal: option_le (p_term_assignment qic f (@subst variable function constructor s t)) (p_term_assignment qic f (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f0 lp t)))) *)
        (pi:=cbv_update n v1 pi c0 s c3 u) (proof_tree:=proof_tree);auto.
(* Goal: valid_QI qic qif cs *)
  unfold valid_QI;tauto.
- apply Plus.plus_le_compat_r;apply Mult.mult_le_compat_l.
  unfold proof_tree in *;clear proof_tree.
  unfold t in *;clear t.
(* Goal: le (term_assignment qic qif (@fapply variable function constructor f lv)) (qif f l) *)
  simpl in well_formed.
(* Goal: le (term_assignment qic qif (@fapply variable function constructor f lv)) (qif f l) *)
  destruct well_formed as (_ & lp0 & t' & _ & _ & Hlv & _ & _ & _ & _ & _ & wfp & _).
(* Goal: option_le (p_term_assignment qic f (@subst variable function constructor s t)) (p_term_assignment qic f (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f0 lp t)))) *)
  apply (qi_active_bounded_by_size qic qif cs) with (lval:=map (psubst sub) lp0) (lt:=lv);auto.
(* Goal: valid_QI qic qif cs *)
  unfold valid_QI;tauto.
Qed.

Lemma active_size_bound_max qic qif cs: forall i s p c f lv d v,
  valid_QI qic qif cs ->
  let t :=  (fapply f lv) in
  let pi := cbv_update i s p c t d v in 
  let la := (activations pi)  in
  let l:= (map (fun x=> mcs * (term_size t)) lv) in
  wf pi -> cache_bounded qic qif c -> forall la', incl la' la -> 
  maxl (map judgsize la') <= (max_arity + 1) * qif f l + 1.
Proof.
(* Goal: forall (i : nat) (s : forall _ : variable, Syntax.value constructor) (p : CBV_cache.cbv variable function constructor) (c : CBV_cache.cache variable function constructor) (f : function) (lv : list (Syntax.term variable function constructor)) (d : CBV_cache.cache variable function constructor) (v : Syntax.value constructor) (_ : valid_QI qic qif cs), let t := @fapply variable function constructor f lv in let pi := @cbv_update variable function constructor i s p c t d v in let la := @activations variable function constructor pi in let l := @map (Syntax.term variable function constructor) nat (fun _ : Syntax.term variable function constructor => Init.Nat.mul mcs (@term_size variable function constructor t)) lv in forall (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity pi) (_ : cache_bounded qic qif c) (la' : list (CBV_cache.cbv variable function constructor)) (_ : @incl (CBV_cache.cbv variable function constructor) la' la), le (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize la')) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (S O)) (qif f l)) (S O)) *)
intros i s p c f lv d v valid t pi la l Hwf Hcb la' Hsslist.
(* Goal: @eq (option nat) (p_term_assignment qic qif (@Syntax.term_from_value variable function constructor (@c_capply constructor c l))) (@Some nat (value_assignment qic (@c_capply constructor c l))) *)
induction la';simpl.
- apply le_0_n.
- apply max_lub.
  + apply (active_size_bound qic qif cs i s p c f lv d v a);auto.
(* Goal: @In (CBV_cache.cbv variable function constructor) a (@activations variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) *)
    apply (Hsslist a);apply in_eq.
  + apply IHla'.
(* Goal: @incl (CBV_cache.cbv variable function constructor) lp' lp *)
    apply tl_incl with (a:=a);trivial.
Qed.

Lemma max_active_size_sublist: forall c c' lp lp',
  andl (map wf lp) -> cache_path c c' lp = true -> incl lp' lp ->
  (forall p : cbv, In p lp -> wf p ->
   max_active_size p <= maxl (map judgsize (activations p))) ->
   maxl (map (@max_active_size _ _ _) lp') <= 
   maxl (map judgsize (flat_map (activations (constructor:=constructor)) lp')).
Proof.
(* Goal: forall (c c' : CBV_cache.cache variable function constructor) (lp lp' : list (CBV_cache.cbv variable function constructor)) (_ : andl (@map (CBV_cache.cbv variable function constructor) Prop (@CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity) lp)) (_ : @eq bool (@CBV_cache.cache_path variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec c c' lp) true) (_ : @incl (CBV_cache.cbv variable function constructor) lp' lp) (_ : forall (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p lp) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p), le (@max_active_size variable function constructor p) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor p)))), le (maxl (@map (CBV_cache.cbv variable function constructor) nat (@max_active_size variable function constructor) lp')) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (@activations variable function constructor) lp'))) *)
induction lp'.
- (* induction : nil *)
(* Goal: option_le (p_term_assignment qic f (@subst variable function constructor s t)) (p_term_assignment qic f (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f0 lp t)))) *)
  simpl;intros;auto. 
- (* induction : cons *)
(* Goal: forall _ : le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)))), le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (Datatypes.S O)) (qif f l)) (Datatypes.S O)) *)
  intros.
(* Goal: @eq (option nat) (p_term_assignment qic qif (@Syntax.term_from_value variable function constructor (@c_capply constructor c l))) (@Some nat (value_assignment qic (@c_capply constructor c l))) *)
  simpl.
(* Goal: le (Nat.max (@max_active_size variable function constructor pi) (maxl (@map (CBV_cache.cbv variable function constructor) nat (@max_active_size variable function constructor) lp))) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@app (CBV_cache.cbv variable function constructor) (@activations variable function constructor pi) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (@activations variable function constructor) lp)))) *)
  rewrite map_app.
(* Goal: le (Nat.max (@max_active_size variable function constructor pi) (maxl (@map (CBV_cache.cbv variable function constructor) nat (@max_active_size variable function constructor) lp))) (maxl (@app nat (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor pi)) (@map (CBV_cache.cbv variable function constructor) nat judgsize (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (@activations variable function constructor) lp)))) *)
  rewrite maxl_app.
(* Goal: le (Nat.max (@max_active_size variable function constructor pi) (maxl (@map (CBV_cache.cbv variable function constructor) nat (@max_active_size variable function constructor) lp))) (Nat.max (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor pi))) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (@activations variable function constructor) lp)))) *)
  apply Nat.max_le_compat.
  + (* cas gauche du max_le_compat *)
(* Goal: le (@max_active_size variable function constructor a) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor a))) *)
    apply (H2 a).
(* Goal: le (term_assignment qic qif t) (qif f (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) lt)) *)
    unfold incl in H1;apply H1;simpl;auto.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity a *)
    apply andl_in_map with (l:=lp);auto.
(* Goal: le (term_assignment qic qif t) (qif f (@map (Syntax.term variable function constructor) nat (term_assignment qic qif) lt)) *)
    unfold incl in H1;apply (H1 a);simpl;auto.
  + (* cas droite du max_le_compat *)
(* Goal: option_le (p_term_assignment qic f (@subst variable function constructor s t)) (p_term_assignment qic f (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f0 lp t)))) *)
    apply IHlp';intros;auto.
(* Goal: @incl (CBV_cache.cbv variable function constructor) lp' lp *)
    apply tl_incl with (a:=a);trivial.
Qed.

Lemma max_active_size_is_max: forall pi,
   let S := max_active_size pi in
   wf pi -> S <= maxl (map judgsize (activations pi)).
Proof.
(* Goal: option_le (p_term_assignment qic f (@subst variable function constructor s t)) (p_term_assignment qic f (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f0 lp t)))) *)
induction pi using cbv_ind2;intros;auto.
- (* cas cbv_constr *)
(* Goal: @eq (option nat) (p_term_assignment qic qif (@Syntax.term_from_value variable function constructor (@c_capply constructor c l))) (@Some nat (value_assignment qic (@c_capply constructor c l))) *)
  unfold S;simpl.  
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
  simpl in H0;destruct t;destruct v;try tauto.
(* Goal: le (maxl (@map (CBV_cache.cbv variable function constructor) nat (@max_active_size variable function constructor) lp)) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (@activations variable function constructor) lp))) *)
  destruct H0 as (cpath & Hc & HGl & Hl0 & wf_list & arity).
(* Goal: option_le (p_term_assignment qic f (@subst variable function constructor s t)) (p_term_assignment qic f (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f0 lp t)))) *)
  apply max_active_size_sublist with (c:=c1) (c':=c2) (lp:=lp);auto.
(* Goal: @incl (CBV_cache.cbv variable function constructor) (@activations variable function constructor pi) (@activations variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) *)
  apply incl_refl.
- (* cas cbv_split *)
(* Goal: @eq (option nat) (p_term_assignment qic qif (@Syntax.term_from_value variable function constructor (@c_capply constructor c l))) (@Some nat (value_assignment qic (@c_capply constructor c l))) *)
  unfold S;simpl.
(* Goal: le (Nat.max (@max_active_size variable function constructor pi) (maxl (@map (CBV_cache.cbv variable function constructor) nat (@max_active_size variable function constructor) lp))) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@app (CBV_cache.cbv variable function constructor) (@activations variable function constructor pi) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (@activations variable function constructor) lp)))) *)
  rewrite map_app.
(* Goal: le (Nat.max (@max_active_size variable function constructor pi) (maxl (@map (CBV_cache.cbv variable function constructor) nat (@max_active_size variable function constructor) lp))) (maxl (@app nat (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor pi)) (@map (CBV_cache.cbv variable function constructor) nat judgsize (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (@activations variable function constructor) lp)))) *)
  rewrite maxl_app.  
(* Goal: le (Nat.max (@max_active_size variable function constructor pi) (maxl (@map (CBV_cache.cbv variable function constructor) nat (@max_active_size variable function constructor) lp))) (Nat.max (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor pi))) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (@activations variable function constructor) lp)))) *)
  apply Nat.max_le_compat.
  + (* le sous arbre isolé *)
(* Goal: le (@max_active_size variable function constructor pi) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor pi))) *)
    apply IHpi.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity pi *)
    simpl in H0.
(* Goal: option_le (p_term_assignment qic f (@subst variable function constructor s t)) (p_term_assignment qic f (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f0 lp t)))) *)
    destruct pi;destruct t0;destruct t;tauto.
  + (* la liste de sous-arbres *)
    simpl in H0;destruct pi;destruct t0;destruct t;try tauto;
          destruct H0 as (Hc & cpath & Hl0 & Hl & wf_list & Hf & Hv & wfp & arity);
(* Goal: @incl (CBV_cache.cbv variable function constructor) (@activations variable function constructor pi) (@activations variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) *)
          apply max_active_size_sublist with (c:=c1) (c':=c) (lp:=lp);auto;apply incl_refl.
- (* cas cbv_update *)
(* Goal: le S (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor (@cbv_update variable function constructor n s pi c1 t c2 v)))) *)
  simpl activations.
(* Goal: le S (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@cons (CBV_cache.cbv variable function constructor) (@cbv_update variable function constructor n s pi c1 t c2 v) (@activations variable function constructor pi)))) *)
  rewrite map_cons.
(* Goal: le S (maxl (@cons nat (judgsize (@cbv_update variable function constructor n s pi c1 t c2 v)) (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor pi)))) *)
  simpl maxl.
(* Goal: le S (Nat.max (judgsize (@cbv_update variable function constructor n s pi c1 t c2 v)) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor pi)))) *)
  simpl in S.
(* Goal: option_le (p_term_assignment qic f (@subst variable function constructor s t)) (p_term_assignment qic f (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f0 lp t)))) *)
  apply Nat.max_le_compat;auto.
(* Goal: le (@max_active_size variable function constructor pi) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor pi))) *)
  apply IHpi.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity pi *)
  simpl in H.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity pi *)
  destruct t;try tauto.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity pi *)
  destruct H as (_ & _ & _ & _ & _ & _ & _ & _ & _ & _ & _ & H & _);trivial.
Qed.

Theorem max_active_size_bound qic qif cs: forall i s p c f lv d v,
  valid_QI qic qif cs ->
  let t :=  (fapply f lv) in
  let pi := cbv_update i s p c t d v in 
  let l:= (map (fun x=> mcs * (term_size t)) lv) in
  let S := max_active_size pi in
  wf pi -> cache_bounded qic qif c -> S <= (max_arity + 1) * (qif f l) + 1.
Proof.
(* Goal: forall _ : le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)))), le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (Datatypes.S O)) (qif f l)) (Datatypes.S O)) *)
intros i s p c f lv d v valid;intros.
(* Goal: le S (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (Datatypes.S O)) (qif f l)) (Datatypes.S O)) *)
generalize (max_active_size_is_max pi H).
(* Goal: forall _ : le (@max_active_size variable function constructor pi) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor pi))), le S (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (Datatypes.S O)) (qif f l)) (Datatypes.S O)) *)
unfold S, pi,t.
(* Goal: forall _ : le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (maxl (@map (CBV_cache.cbv variable function constructor) nat judgsize (@activations variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)))), le (@max_active_size variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) (Init.Nat.add (Init.Nat.mul (Init.Nat.add max_arity (Datatypes.S O)) (qif f l)) (Datatypes.S O)) *)
intros.
(* Goal: option_le (p_term_assignment qic f (@subst variable function constructor s t)) (p_term_assignment qic f (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f0 lp t)))) *)
apply le_trans with (m:=maxl (map judgsize (activations pi)));auto.
(* Goal: option_le (p_term_assignment qic f (@subst variable function constructor s t)) (p_term_assignment qic f (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f0 lp t)))) *)
apply (active_size_bound_max qic qif cs i s p c f lv d v);auto.
(* Goal: @incl (CBV_cache.cbv variable function constructor) (@activations variable function constructor pi) (@activations variable function constructor (@cbv_update variable function constructor i s p c (@fapply variable function constructor f lv) d v)) *)
apply incl_refl.
Qed.

(* partial version of compatible QI *)

Definition p_assignment_function := function -> option(list nat -> nat).

(* partial assignment of a term*)
Fixpoint p_term_assignment (qic:assignment_constructor) (qif:p_assignment_function)
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
(t:term) {struct t} : option nat:=
   match t with
  | var v=> Some 0 (* pas necessaire. Les QI sont toujours appliquées sur des termes clots. *)
  | capply c lt => option_map (qic c) (option_list_map(map (p_term_assignment qic qif) lt))
  | fapply f lt=> option_bind (fun g => option_map g (option_list_map(map (p_term_assignment qic qif)  lt)))
                              (qif f)
end.

Definition complete_p_QI (qif : p_assignment_function) f := 
  complete_option maxl (qif f).

Lemma p_term_assignment_term_assignment qic qif t v:
  p_term_assignment qic qif t = Some v ->
  term_assignment qic (complete_p_QI qif) t = v.
Proof.
revert v; induction t using term_ind2.
- intros n H; now inversion H.
- unfold option_map; intros v H0; simpl p_term_assignment in H0.
  simpl term_assignment.
  case_eq (option_list_map (map (p_term_assignment qic qif) l));
    [| intro H1; rewrite H1 in H0; inversion H0].
  intros lv Hlv.
  rewrite option_list_map_map with (f := complete_option 0) in H0.
  + simpl option_map in H0; inversion H0.
    rewrite map_map; f_equal; apply map_ext_in; intros a Ha.
    apply option_list_map_Some with (x := p_term_assignment qic qif a) in Hlv.
    * destruct Hlv as (va & Hva); rewrite Hva; auto.
    * now apply in_map.
  + intros x Hx.
(* Goal: option_le (p_term_assignment qic f (@subst variable function constructor s t)) (p_term_assignment qic f (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f0 lp t)))) *)
    eapply option_list_map_Some in Hlv; eauto.
    now destruct Hlv as [vx Hvx]; rewrite Hvx.
- unfold option_map, complete_p_QI; intros v H0; simpl p_term_assignment in H0.
  case_eq (qif f); [ | intro Hf; rewrite Hf in H0; inversion H0].
  intros g Hg; rewrite Hg in *; simpl in H0.
  simpl term_assignment.
  case_eq (option_list_map (map (p_term_assignment qic qif) l));
    [| intro H1; rewrite H1 in H0; inversion H0].
  intros lv Hlv.
(* Goal: @eq (option nat) (p_term_assignment qic qif (@Syntax.term_from_value variable function constructor (@c_capply constructor c l))) (@Some nat (value_assignment qic (@c_capply constructor c l))) *)
  rewrite Hg; simpl.
  rewrite Hlv in H0.
  inversion H0.
  subst v.
  f_equal.
  assert(Heq : Some (map
  (term_assignment qic
     (fun f0 : function => complete_option maxl (qif f0)))
  l) = Some lv); [ | now inversion Heq].
  rewrite <- Hlv.
  erewrite option_list_map_map.
(* Goal: @eq (option nat) match (fix option_list_map (A : Type) (l : list (option A)) {struct l} : option (list A) := match l with | nil => @Some (list A) (@nil A) | cons (Some h as o) t => @option_map (list A) (list A) (@cons A h) (option_list_map A t) | cons (None as o) t => @None (list A) end) nat (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic qif) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor) l)) with | Some a => @Some nat (qic c a) | None => @None nat end (@Some nat (qic c (@map (Syntax.value constructor) nat (value_assignment qic) l))) *)
  + rewrite map_map.
    instantiate (1 := complete_option 0).
    f_equal.
(* Goal: @eq (list (option nat)) (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) f g)) l) (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic f) l) *)
    apply map_ext_in.
(* Goal: forall (a : Syntax.term variable function constructor) (_ : @In (Syntax.term variable function constructor) a l), @eq (option nat) (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) f g) a) (p_term_assignment qic f a) *)
    intros a Ha.
    apply option_list_map_Some with (x := p_term_assignment qic qif a) in Hlv.
    * destruct Hlv as (va & Hva); rewrite Hva; auto.
    * now apply in_map.
  + intros x Hx.
(* Goal: option_le (p_term_assignment qic f (@subst variable function constructor s t)) (p_term_assignment qic f (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f0 lp t)))) *)
    eapply option_list_map_Some in Hlv; eauto.
    now destruct Hlv as [vx Hvx]; rewrite Hvx.
Qed.

Definition p_compatible_QI qic qif:= forall f lp t, forall s:variable -> value,
  let ru := rule_intro f lp t in
  (In ru prog) -> 
    p_term_assignment qic qif (subst s t) ≤p 
    p_term_assignment qic qif (subst s (lhs_of_rule ru)).

Lemma p_compatible_compatible qic:
  {pqif | p_compatible_QI qic pqif} -> {qif | compatible_QI qic qif}.
Proof.
(* Goal: forall _ : @sig p_assignment_function (fun pqif : p_assignment_function => p_compatible_QI qic pqif), @sig assignment_function (fun qif : assignment_function => compatible_QI qic qif) *)
unfold compatible_QI, p_compatible_QI.
(* Goal: forall _ : @sig p_assignment_function (fun pqif : p_assignment_function => forall (f : function) (lp : list (Syntax.pattern variable constructor)) (t : Syntax.term variable function constructor) (s : forall _ : variable, Syntax.value constructor) (_ : @In (Syntax.rule variable function constructor) (@rule_intro variable function constructor f lp t) prog), option_le (p_term_assignment qic pqif (@subst variable function constructor s t)) (p_term_assignment qic pqif (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f lp t))))), @sig assignment_function (fun qif : assignment_function => forall (f : function) (lp : list (Syntax.pattern variable constructor)) (t : Syntax.term variable function constructor) (s : forall _ : variable, Syntax.value constructor) (_ : @In (Syntax.rule variable function constructor) (@rule_intro variable function constructor f lp t) prog), le (term_assignment qic qif (@subst variable function constructor s t)) (term_assignment qic qif (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f lp t))))) *)
intros [qif H]; exists (complete_p_QI qif).
(* Goal: forall (f : function) (lp : list (Syntax.pattern variable constructor)) (t : Syntax.term variable function constructor) (s : forall _ : variable, Syntax.value constructor) (_ : @In (Syntax.rule variable function constructor) (@rule_intro variable function constructor f lp t) prog), le (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s t)) (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f lp t)))) *)
intros f lp t s Hr.
(* Goal: le (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s t)) (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f lp t)))) *)
assert (H' := H f lp t s Hr).
(* Goal: le (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s t)) (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f lp t)))) *)
destruct H' as (v1 & v2 & Hv1 & Hv2 & Heq).
(* Goal: le (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s t)) (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f lp t)))) *)
apply p_term_assignment_term_assignment in Hv1.
(* Goal: le (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s t)) (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f lp t)))) *)
apply p_term_assignment_term_assignment in Hv2.
(* Goal: le (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s t)) (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f lp t)))) *)
now subst.
Qed.

Lemma p_term_assignment_ext qic f f': 
 (forall x, f x = f' x) ->
 forall t, p_term_assignment qic f t= p_term_assignment qic f' t.
Proof.
(* Goal: forall (_ : forall x : function, @eq (option (forall _ : list nat, nat)) (f x) (f' x)) (t : Syntax.term variable function constructor), @eq (option nat) (p_term_assignment qic f t) (p_term_assignment qic f' t) *)
intro Heq.
(* Goal: forall (v : nat) (_ : @eq (option nat) (p_term_assignment qic f t) (@Some nat v)) (g : forall _ : function, option (forall _ : list nat, nat)), @eq (option nat) (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) f g) t) (@Some nat v) *)
induction t using term_ind2.
- trivial.
- simpl p_term_assignment; f_equal; f_equal; now apply map_ext_in.
- simpl p_term_assignment.
  rewrite <- Heq.
(* Goal: @eq (option nat) (p_term_assignment qic f (@var variable function constructor x)) (p_term_assignment qic f' (@var variable function constructor x)) *)
  destruct (f f0) as [v |]; trivial.
(* Goal: @eq (list (option nat)) (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) f g)) l) (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic f) l) *)
  simpl; f_equal; f_equal; now apply map_ext_in.
Qed.

Lemma p_compatible_QI_ext qic f f': 
 (forall x, f x = f' x) ->
 p_compatible_QI qic f ->
 p_compatible_QI qic f'.
Proof.
intros Heq Hf; unfold p_compatible_QI in *.
intros;
do 2(rewrite <- p_term_assignment_ext with (f := f) (f' := f'); trivial).
(* Goal: option_le (p_term_assignment qic f (@subst variable function constructor s t)) (p_term_assignment qic f (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f0 lp t)))) *)
auto.
Qed.

Lemma p_compatible_QI_split qic f h:
  {g | p_compatible_QI qic (f;;h;;g)} -> {g | p_compatible_QI qic (f;;g)}.
Proof.
- intro H.
(* Goal: @sig (forall _ : function, option (forall _ : list nat, nat)) (fun g : forall _ : function, option (forall _ : list nat, nat) => p_compatible_QI qic (@option_choice function (forall _ : list nat, nat) f g)) *)
destruct H as (g & Hhg).
(* Goal: @sig (forall _ : function, option (forall _ : list nat, nat)) (fun g : forall _ : function, option (forall _ : list nat, nat) => p_compatible_QI qic (@option_choice function (forall _ : list nat, nat) f g)) *)
exists (h;;g); eapply p_compatible_QI_ext; [ | exact Hhg].
(* Goal: forall x : function, @eq (option (forall _ : list nat, nat)) (@option_choice function (forall _ : list nat, nat) (@option_choice function (forall _ : list nat, nat) f h) g x) (@option_choice function (forall _ : list nat, nat) f (@option_choice function (forall _ : list nat, nat) h g) x) *)
intro; now rewrite option_choice_assoc.
Qed.

Lemma p_term_assignment_first_choice qic f t v:
  p_term_assignment qic f t = Some v ->
  forall g, p_term_assignment qic (f;;g) t = Some v.
Proof.
(* Goal: forall (_ : @eq (option nat) (p_term_assignment qic f t) (@Some nat v)) (g : forall _ : function, option (forall _ : list nat, nat)), @eq (option nat) (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) f g) t) (@Some nat v) *)
revert v.
(* Goal: forall (v : nat) (_ : @eq (option nat) (p_term_assignment qic f t) (@Some nat v)) (g : forall _ : function, option (forall _ : list nat, nat)), @eq (option nat) (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) f g) t) (@Some nat v) *)
induction t using term_ind2.
- intros; assumption.
- intros v Hv g; simpl in *.
  rewrite <- Hv; do 2 f_equal.
(* Goal: forall (a : Syntax.term variable function constructor) (_ : @In (Syntax.term variable function constructor) a l), @eq (option nat) (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) f g) a) (p_term_assignment qic f a) *)
  apply map_ext_in; intros a Ha.
(* Goal: @eq (option nat) (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) f g) a) (p_term_assignment qic f a) *)
  apply option_map_Some in Hv; destruct Hv as (v' & Hv').
  apply option_list_map_Some with (x := p_term_assignment qic f a) in Hv';
  [ | now apply in_map].
(* Goal: @eq (option nat) (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) f g) a) (p_term_assignment qic f a) *)
  destruct Hv' as (v'' & Hv''); rewrite Hv''.
(* Goal: @eq (option nat) (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) f g) a) (@Some nat v'') *)
  apply H; assumption.
- intros v Hv g; simpl in *.
  rewrite <- Hv.
(* Goal: @eq (option nat) (@option_bind (forall _ : list nat, nat) nat (fun g0 : forall _ : list nat, nat => @option_map (list nat) nat g0 (@option_list_map nat (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) f g)) l))) (@option_choice function (forall _ : list nat, nat) f g f0)) (@option_bind (forall _ : list nat, nat) nat (fun g : forall _ : list nat, nat => @option_map (list nat) nat g (@option_list_map nat (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic f) l))) (f f0)) *)
  simpl option_choice.
(* Goal: @eq (option nat) (@option_bind (forall _ : list nat, nat) nat (fun g0 : forall _ : list nat, nat => @option_map (list nat) nat g0 (@option_list_map nat (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) f g)) l))) (@option_choice function (forall _ : list nat, nat) f g f0)) (@option_bind (forall _ : list nat, nat) nat (fun g : forall _ : list nat, nat => @option_map (list nat) nat g (@option_list_map nat (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic f) l))) (f f0)) *)
  case_eq (f f0); [| intro Hnone; rewrite Hnone in Hv; inversion Hv].
(* Goal: forall (n : forall _ : list nat, nat) (_ : @eq (option (forall _ : list nat, nat)) (f f0) (@Some (forall _ : list nat, nat) n)), @eq (option nat) (@option_bind (forall _ : list nat, nat) nat (fun g0 : forall _ : list nat, nat => @option_map (list nat) nat g0 (@option_list_map nat (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) f g)) l))) (@option_choice function (forall _ : list nat, nat) f g f0)) (@option_bind (forall _ : list nat, nat) nat (fun g : forall _ : list nat, nat => @option_map (list nat) nat g (@option_list_map nat (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic f) l))) (@Some (forall _ : list nat, nat) n)) *)
  intros v' Hv'.
  assert (Hfg : (f;; g) f0 = Some v') by
    (unfold option_choice; now rewrite Hv').
(* Goal: @eq (option nat) (@option_bind (forall _ : list nat, nat) nat (fun g0 : forall _ : list nat, nat => @option_map (list nat) nat g0 (@option_list_map nat (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) f g)) l))) (@option_choice function (forall _ : list nat, nat) f g f0)) (@option_bind (forall _ : list nat, nat) nat (fun g : forall _ : list nat, nat => @option_map (list nat) nat g (@option_list_map nat (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic f) l))) (@Some (forall _ : list nat, nat) v')) *)
  rewrite Hfg.
(* Goal: @eq (option nat) (p_term_assignment qic qif (@Syntax.term_from_value variable function constructor (@c_capply constructor c l))) (@Some nat (value_assignment qic (@c_capply constructor c l))) *)
  simpl.
  do 2 f_equal.
(* Goal: @eq (list (option nat)) (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) f g)) l) (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic f) l) *)
  apply map_ext_in.
(* Goal: forall (a : Syntax.term variable function constructor) (_ : @In (Syntax.term variable function constructor) a l), @eq (option nat) (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) f g) a) (p_term_assignment qic f a) *)
  intros a Ha.
(* Goal: @eq (option nat) (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) f g) a) (p_term_assignment qic f a) *)
  apply option_bind_Some in Hv.
(* Goal: @eq (option nat) (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) f g) a) (p_term_assignment qic f a) *)
  destruct Hv as (v'' & _ & Hv).
(* Goal: @eq (option nat) (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) f g) a) (p_term_assignment qic f a) *)
  apply option_map_Some in Hv.
(* Goal: @eq (option nat) (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) f g) a) (p_term_assignment qic f a) *)
  destruct Hv as (v'''' & Hv).
(* Goal: @eq (option nat) (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) f g) a) (p_term_assignment qic f a) *)
  apply option_list_map_Some with (x := p_term_assignment qic f a) in Hv.
  + destruct Hv as (lv & Hlv).
(* Goal: option_le (p_term_assignment qic f (@subst variable function constructor s t)) (p_term_assignment qic f (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f0 lp t)))) *)
    erewrite H; eauto.
  + now apply in_map.
Qed.

Lemma value_as_p_term_assignment qic qif: forall v:value,
  (p_term_assignment qic qif (term_from_value v)) = Some (value_assignment qic v).
Proof.
(* Goal: forall v : Syntax.value constructor, @eq (option nat) (p_term_assignment qic qif (@Syntax.term_from_value variable function constructor v)) (@Some nat (value_assignment qic v)) *)
induction v using value_ind2.
(* Goal: @eq (option nat) (p_term_assignment qic qif (@Syntax.term_from_value variable function constructor (@c_capply constructor c l))) (@Some nat (value_assignment qic (@c_capply constructor c l))) *)
simpl.
(* Goal: @eq (option nat) (@option_map (list nat) nat (qic c) (@option_list_map nat (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic qif) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor) l)))) (@Some nat (qic c (@map (Syntax.value constructor) nat (value_assignment qic) l))) *)
unfold option_map, option_list_map.
(* Goal: @eq (option nat) match (fix option_list_map (A : Type) (l : list (option A)) {struct l} : option (list A) := match l with | nil => @Some (list A) (@nil A) | cons (Some h as o) t => @option_map (list A) (list A) (@cons A h) (option_list_map A t) | cons (None as o) t => @None (list A) end) nat (@map (Syntax.term variable function constructor) (option nat) (p_term_assignment qic qif) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@Syntax.term_from_value variable function constructor) l)) with | Some a => @Some nat (qic c a) | None => @None nat end (@Some nat (qic c (@map (Syntax.value constructor) nat (value_assignment qic) l))) *)
rewrite map_map.
rewrite option_list_map_map with 
  (f := fun x => match x with Some v => v | None => 0 end).
- do 2 f_equal; rewrite map_map; apply map_ext_in.
(* Goal: @eq (option nat) (p_term_assignment qic f (@var variable function constructor x)) (p_term_assignment qic f' (@var variable function constructor x)) *)
  intros; rewrite H; trivial.
- intros x Hx.
(* Goal: @eq (option nat) x (@Some nat match x with | Some v => v | None => O end) *)
  apply in_map_iff in Hx.
(* Goal: @eq (option nat) x (@Some nat match x with | Some v => v | None => O end) *)
  destruct Hx as (n & Hn1 & Hn2).
(* Goal: @eq (option nat) (p_term_assignment qic f (@var variable function constructor x)) (p_term_assignment qic f' (@var variable function constructor x)) *)
  rewrite H in Hn1; trivial.
  rewrite <- Hn1; trivial.
Qed.

Definition p_subterm (qif : p_assignment_function) : Prop :=
forall (f : function) (l : list nat) (x : nat), x ∈ l ->
  match qif f with 
  | None => True 
  | Some f0 => (x <= f0 l)
  end.

Definition p_monotonicity (qif : p_assignment_function) : Prop :=
  forall (f : function) (lx ly : list nat),
    Forall2 le lx ly -> 
    match qif f with 
    | None => True 
    | Some f0 => f0 lx <= f0 ly
    end.

Definition p_smc qic (qif : p_assignment_function) : Prop :=
 p_subterm qif /\ p_monotonicity qif /\ p_compatible_QI qic qif.

Lemma p_smc_split f h qic:
  {g | p_smc qic (f;;h;;g)} -> {g | p_smc qic (f;;g)}.
Proof.
(* Goal: forall _ : @sig (forall _ : function, option (forall _ : list nat, nat)) (fun g : forall _ : function, option (forall _ : list nat, nat) => p_smc qic (@option_choice function (forall _ : list nat, nat) (@option_choice function (forall _ : list nat, nat) f h) g)), @sig (forall _ : function, option (forall _ : list nat, nat)) (fun g : forall _ : function, option (forall _ : list nat, nat) => p_smc qic (@option_choice function (forall _ : list nat, nat) f g)) *)
intro H.
unfold p_smc in *.
(* Goal: @sig (forall _ : function, option (forall _ : list nat, nat)) (fun g : forall _ : function, option (forall _ : list nat, nat) => and (p_subterm (@option_choice function (forall _ : list nat, nat) f g)) (and (p_monotonicity (@option_choice function (forall _ : list nat, nat) f g)) (p_compatible_QI qic (@option_choice function (forall _ : list nat, nat) f g)))) *)
destruct H as (g & Hhgs & Hhgm & Hhgc).
(* Goal: @sig (forall _ : function, option (forall _ : list nat, nat)) (fun g : forall _ : function, option (forall _ : list nat, nat) => and (p_subterm (@option_choice function (forall _ : list nat, nat) f g)) (and (p_monotonicity (@option_choice function (forall _ : list nat, nat) f g)) (p_compatible_QI qic (@option_choice function (forall _ : list nat, nat) f g)))) *)
exists (h;;g).
unfold p_subterm, p_monotonicity, p_compatible_QI in *.
(* Goal: and (forall (f0 : function) (l : list nat) (x : nat) (_ : @In nat x l), match @option_choice function (forall _ : list nat, nat) f (@option_choice function (forall _ : list nat, nat) h g) f0 with | Some f1 => le x (f1 l) | None => True end) (and (forall (f0 : function) (lx ly : list nat) (_ : @Forall2 nat nat le lx ly), match @option_choice function (forall _ : list nat, nat) f (@option_choice function (forall _ : list nat, nat) h g) f0 with | Some f1 => le (f1 lx) (f1 ly) | None => True end) (forall (f0 : function) (lp : list (Syntax.pattern variable constructor)) (t : Syntax.term variable function constructor) (s : forall _ : variable, Syntax.value constructor) (_ : @In (Syntax.rule variable function constructor) (@rule_intro variable function constructor f0 lp t) prog), option_le (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) f (@option_choice function (forall _ : list nat, nat) h g)) (@subst variable function constructor s t)) (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) f (@option_choice function (forall _ : list nat, nat) h g)) (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f0 lp t)))))) *)
repeat split; intros f0 l x Hin.
- assert (H := Hhgs f0 l x Hin); now rewrite <- option_choice_assoc in H.
- assert (H := Hhgm f0 l x Hin); now rewrite <- option_choice_assoc in H.
- eapply p_compatible_QI_ext; [ | exact Hhgc]; intro; now rewrite option_choice_assoc.
Qed.

Lemma p_smc_smc qic :
  {pqif | p_smc qic ((fun _ => None);; pqif)} -> 
(* Goal: cache_bounded qic qif (@cache_left variable function constructor pi) *)
  {qif | subterm qif /\ monotonicity_qif qif /\ compatible_QI qic qif}.
Proof.
unfold p_smc, compatible_QI, p_compatible_QI, p_subterm, subterm, 
       monotonicity_qif, p_monotonicity.
(* Goal: forall _ : @sig (forall _ : function, option (forall _ : list nat, nat)) (fun pqif : forall _ : function, option (forall _ : list nat, nat) => and (forall (f : function) (l : list nat) (x : nat) (_ : @In nat x l), match @option_choice function (forall _ : list nat, nat) (fun _ : function => @None (forall _ : list nat, nat)) pqif f with | Some f0 => le x (f0 l) | None => True end) (and (forall (f : function) (lx ly : list nat) (_ : @Forall2 nat nat le lx ly), match @option_choice function (forall _ : list nat, nat) (fun _ : function => @None (forall _ : list nat, nat)) pqif f with | Some f0 => le (f0 lx) (f0 ly) | None => True end) (forall (f : function) (lp : list (Syntax.pattern variable constructor)) (t : Syntax.term variable function constructor) (s : forall _ : variable, Syntax.value constructor) (_ : @In (Syntax.rule variable function constructor) (@rule_intro variable function constructor f lp t) prog), option_le (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) (fun _ : function => @None (forall _ : list nat, nat)) pqif) (@subst variable function constructor s t)) (p_term_assignment qic (@option_choice function (forall _ : list nat, nat) (fun _ : function => @None (forall _ : list nat, nat)) pqif) (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f lp t))))))), @sig assignment_function (fun qif : assignment_function => and (forall (f : function) (l : list nat) (x : nat) (_ : @In nat x l), le x (qif f l)) (and (forall (f : function) (lx ly : list nat) (_ : @Forall2 nat nat le lx ly), le (qif f lx) (qif f ly)) (forall (f : function) (lp : list (Syntax.pattern variable constructor)) (t : Syntax.term variable function constructor) (s : forall _ : variable, Syntax.value constructor) (_ : @In (Syntax.rule variable function constructor) (@rule_intro variable function constructor f lp t) prog), le (term_assignment qic qif (@subst variable function constructor s t)) (term_assignment qic qif (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f lp t))))))) *)
intros (qif & Hs & Hm & Hc); exists (complete_p_QI qif).
(* Goal: and (forall (f : function) (l : list nat) (x : nat) (_ : @In nat x l), le x (complete_p_QI qif f l)) (and (forall (f : function) (lx ly : list nat) (_ : @Forall2 nat nat le lx ly), le (complete_p_QI qif f lx) (complete_p_QI qif f ly)) (forall (f : function) (lp : list (Syntax.pattern variable constructor)) (t : Syntax.term variable function constructor) (s : forall _ : variable, Syntax.value constructor) (_ : @In (Syntax.rule variable function constructor) (@rule_intro variable function constructor f lp t) prog), le (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s t)) (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f lp t)))))) *)
repeat split.
- intros f l x Hin.
(* Goal: le x (complete_p_QI qif f l) *)
  assert (H' := Hs f l x Hin).
(* Goal: le (complete_p_QI qif f l) (complete_p_QI qif f x) *)
  unfold complete_p_QI, complete_option.
(* Goal: le (match qif f with | Some x => x | None => maxl end l) (match qif f with | Some x => x | None => maxl end x) *)
  unfold option_choice in H'.
(* Goal: @eq (option nat) (p_term_assignment qic f (@var variable function constructor x)) (p_term_assignment qic f' (@var variable function constructor x)) *)
  destruct (qif f); trivial.
(* Goal: le (@term_size variable function constructor x) (maxl (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) lt)) *)
  now apply maxl_is_max.
- intros f l x Hin.
(* Goal: le (complete_p_QI qif f l) (complete_p_QI qif f x) *)
  assert (H' := Hm f l x Hin).
(* Goal: le (complete_p_QI qif f l) (complete_p_QI qif f x) *)
  unfold complete_p_QI, complete_option.
(* Goal: le (match qif f with | Some x => x | None => maxl end l) (match qif f with | Some x => x | None => maxl end x) *)
  unfold option_choice in H'.
(* Goal: @eq (option nat) (p_term_assignment qic f (@var variable function constructor x)) (p_term_assignment qic f' (@var variable function constructor x)) *)
  destruct (qif f); trivial.
(* Goal: le (maxl l) (maxl x) *)
  now apply forall2_le_maxl.
- intros f lp t s Hr.
(* Goal: le (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s t)) (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f lp t)))) *)
  assert (H' := Hc f lp t s Hr).
(* Goal: le (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s t)) (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f lp t)))) *)
  destruct H' as (v1 & v2 & Hv1 & Hv2 & Heq).
(* Goal: le (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s t)) (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f lp t)))) *)
  apply p_term_assignment_term_assignment in Hv1.
(* Goal: le (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s t)) (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f lp t)))) *)
  apply p_term_assignment_term_assignment in Hv2.
(* Goal: le (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s t)) (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f lp t)))) *)
  now subst.
Qed.

End QI.

Section Partial_QI.

Variables variable function constructor : Type.

Notation p_compatible_QI := (p_compatible_QI variable function constructor).
Notation term_from_value := (Syntax.term_from_value variable function (constructor:=constructor)).
Notation p_smc := (p_smc variable function constructor).

(* f is the current partial qi, and g is what remains to be defined *)
Lemma p_compatible_QI_app f prog1 prog2 qic:
  p_compatible_QI prog1 qic f ->
  {g | p_compatible_QI prog2 qic (f;;g)} ->
  {g | p_compatible_QI (prog1 ++ prog2) qic (f;;g)}.
Proof.
(* Goal: forall (_ : SerTop.p_compatible_QI variable function constructor prog1 qic f) (_ : @sig (forall _ : function, option (forall _ : list nat, nat)) (fun g : forall _ : function, option (forall _ : list nat, nat) => SerTop.p_compatible_QI variable function constructor prog2 qic (@option_choice function (forall _ : list nat, nat) f g))), @sig (forall _ : function, option (forall _ : list nat, nat)) (fun g : forall _ : function, option (forall _ : list nat, nat) => SerTop.p_compatible_QI variable function constructor (@app (rule variable function constructor) prog1 prog2) qic (@option_choice function (forall _ : list nat, nat) f g)) *)
intros Hf [g Hg]; exists g.
(* Goal: SerTop.p_compatible_QI variable function constructor (@app (rule variable function constructor) prog1 prog2) qic (@option_choice function (forall _ : list nat, nat) f g) *)
unfold p_compatible_QI; intros f0 lp t s Hrule.
(* Goal: option_le (p_term_assignment qic f (@subst variable function constructor s t)) (p_term_assignment qic f (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f0 lp t)))) *)
apply in_app_iff in Hrule; destruct Hrule as [Hr1 | Hr2]; auto.
(* Goal: option_le (p_term_assignment variable function constructor qic (@option_choice function (forall _ : list nat, nat) f g) (@subst variable function constructor s t)) (p_term_assignment variable function constructor qic (@option_choice function (forall _ : list nat, nat) f g) (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f0 lp t)))) *)
eapply (Hf f0 lp t s) in Hr1.
destruct Hr1 as (v1 & v2 & Hv1 & Hv2 & Heq);
exists v1; exists v2; intuition;
now apply p_term_assignment_first_choice.
Qed.

Lemma p_smc_QI_app f prog1 prog2 qic:
  p_compatible_QI prog1 qic f ->
  {g | p_smc prog2 qic (f;;g)} ->
  {g | p_smc (prog1 ++ prog2) qic (f;;g)}.
Proof.
(* Goal: forall (_ : SerTop.p_compatible_QI variable function constructor prog1 qic f) (_ : @sig (forall _ : function, option (forall _ : list nat, nat)) (fun g : forall _ : function, option (forall _ : list nat, nat) => SerTop.p_smc variable function constructor prog2 qic (@option_choice function (forall _ : list nat, nat) f g))), @sig (forall _ : function, option (forall _ : list nat, nat)) (fun g : forall _ : function, option (forall _ : list nat, nat) => SerTop.p_smc variable function constructor (@app (rule variable function constructor) prog1 prog2) qic (@option_choice function (forall _ : list nat, nat) f g)) *)
unfold p_smc.
(* Goal: and (forall (f : function) (l : list nat) (x : nat) (_ : @In nat x l), le x (complete_p_QI qif f l)) (and (forall (f : function) (lx ly : list nat) (_ : @Forall2 nat nat le lx ly), le (complete_p_QI qif f lx) (complete_p_QI qif f ly)) (forall (f : function) (lp : list (Syntax.pattern variable constructor)) (t : Syntax.term variable function constructor) (s : forall _ : variable, Syntax.value constructor) (_ : @In (Syntax.rule variable function constructor) (@rule_intro variable function constructor f lp t) prog), le (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s t)) (term_assignment qic (complete_p_QI qif) (@subst variable function constructor s (@lhs_of_rule variable function constructor (@rule_intro variable function constructor f lp t)))))) *)
intros Hfc (g & Hs & Hm & Hc); exists g; repeat split.
- unfold p_subterm in *; intros h l x Hin.
(* Goal: match @option_choice function (forall _ : list nat, nat) f g h with | Some f0 => le x (f0 l) | None => True end *)
  assert (H' := Hs h l x Hin).
  unfold option_choice in *; destruct (f h); trivial.
- unfold p_monotonicity in *; intros h l x Hin.
(* Goal: match @option_choice function (forall _ : list nat, nat) f g h with | Some f0 => le (f0 l) (f0 x) | None => True end *)
  assert (H' := Hm h l x Hin).
  unfold option_choice in *; destruct (f h); trivial.
- intros f0 lp t s r Hrule.
(* Goal: option_le (p_term_assignment variable function constructor qic (@option_choice function (forall _ : list nat, nat) f g) (@subst variable function constructor s t)) (p_term_assignment variable function constructor qic (@option_choice function (forall _ : list nat, nat) f g) (@subst variable function constructor s (@lhs_of_rule variable function constructor r))) *)
  apply in_app_iff in Hrule; destruct Hrule as [Hr1 | Hr2].
  + eapply (Hfc f0 lp t s) in Hr1.
    destruct Hr1 as (v1 & v2 & Hv1 & Hv2 & Heq);
    exists v1; exists v2; intuition;
    now apply p_term_assignment_first_choice.
  + now apply Hc.
Qed.

End Partial_QI.