Library Coq.romega.ReflOmegaCore

Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable ZArith_base.
Delimit Scope Int_scope with I.


Module Type Int.

  Parameter int : Set.

  Parameter zero : int.
  Parameter one : int.
  Parameter plus : int -> int -> int.
  Parameter opp : int -> int.
  Parameter minus : int -> int -> int.
  Parameter mult : int -> int -> int.

  Notation "0" := zero : Int_scope.
  Notation "1" := one : Int_scope.
  Infix "+" := plus : Int_scope.
  Infix "-" := minus : Int_scope.
  Infix "*" := mult : Int_scope.
  Notation "- x" := (opp x) : Int_scope.

  Open Scope Int_scope.

  Axiom ring : @ring_theory int 0 1 plus mult minus opp (@eq int).


  Parameter le : int -> int -> Prop.
  Parameter lt : int -> int -> Prop.
  Parameter ge : int -> int -> Prop.
  Parameter gt : int -> int -> Prop.
  Notation "x <= y" := (le x y): Int_scope.
  Notation "x < y" := (lt x y) : Int_scope.
  Notation "x >= y" := (ge x y) : Int_scope.
  Notation "x > y" := (gt x y): Int_scope.
  Axiom le_lt_iff : forall i j, (i<=j) <-> ~(j<i).
  Axiom ge_le_iff : forall i j, (i>=j) <-> (j<=i).
  Axiom gt_lt_iff : forall i j, (i>j) <-> (j<i).

  Axiom lt_trans : forall i j k, i<j -> j<k -> i<k.
  Axiom lt_not_eq : forall i j, i<j -> i<>j.

  Axiom lt_0_1 : 0<1.
  Axiom plus_le_compat : forall i j k l, i<=j -> k<=l -> i+k<=j+l.
  Axiom opp_le_compat : forall i j, i<=j -> (-j)<=(-i).
  Axiom mult_lt_compat_l :
   forall i j k, 0 < k -> i < j -> k*i<k*j.

  Parameter compare : int -> int -> comparison.
  Infix "?=" := compare (at level 70, no associativity) : Int_scope.
  Axiom compare_Eq : forall i j, compare i j = Eq <-> i=j.
  Axiom compare_Lt : forall i j, compare i j = Lt <-> i<j.
  Axiom compare_Gt : forall i j, compare i j = Gt <-> i>j.

  Axiom le_lt_int : forall x y, x<y <-> x<=y+-(1).


End Int.


Module Z_as_Int <: Int.

  Open Scope Z_scope.

  Definition int := Z.
  Definition zero := 0.
  Definition one := 1.
  Definition plus := Zplus.
  Definition opp := Zopp.
  Definition minus := Zminus.
  Definition mult := Zmult.

  Lemma ring : @ring_theory int zero one plus mult minus opp (@eq int).

  Definition le := Zle.
  Definition lt := Zlt.
  Definition ge := Zge.
  Definition gt := Zgt.
  Lemma le_lt_iff : forall i j, (i<=j) <-> ~(j<i).
  Definition ge_le_iff := Zge_iff_le.
  Definition gt_lt_iff := Zgt_iff_lt.

  Definition lt_trans := Zlt_trans.
  Definition lt_not_eq := Zlt_not_eq.

  Definition lt_0_1 := Zlt_0_1.
  Definition plus_le_compat := Zplus_le_compat.
  Definition mult_lt_compat_l := Zmult_lt_compat_l.
  Lemma opp_le_compat : forall i j, i<=j -> (-j)<=(-i).

  Definition compare := Zcompare.
  Definition compare_Eq := Zcompare_Eq_iff_eq.
  Lemma compare_Lt : forall i j, compare i j = Lt <-> i<j.
  Lemma compare_Gt : forall i j, compare i j = Gt <-> i>j.

  Lemma le_lt_int : forall x y, x<y <-> x<=y+-(1).

End Z_as_Int.

Module IntProperties (I:Int).
 Import I.


 Definition two := 1+1.
 Notation "2" := two : Int_scope.


 Definition plus_assoc := ring.(Radd_assoc).
 Definition plus_comm := ring.(Radd_comm).
 Definition plus_0_l := ring.(Radd_0_l).
 Definition mult_assoc := ring.(Rmul_assoc).
 Definition mult_comm := ring.(Rmul_comm).
 Definition mult_1_l := ring.(Rmul_1_l).
 Definition mult_plus_distr_r := ring.(Rdistr_l).
 Definition opp_def := ring.(Ropp_def).
 Definition minus_def := ring.(Rsub_def).

 Opaque plus_assoc plus_comm plus_0_l mult_assoc mult_comm mult_1_l
  mult_plus_distr_r opp_def minus_def.


 Lemma plus_0_r : forall x, x+0 = x.

 Lemma plus_0_r_reverse : forall x, x = x+0.

 Lemma plus_assoc_reverse : forall x y z, x+y+z = x+(y+z).

 Lemma plus_permute : forall x y z, x+(y+z) = y+(x+z).

 Lemma plus_reg_l : forall x y z, x+y = x+z -> y = z.


 Lemma mult_assoc_reverse : forall x y z, x*y*z = x*(y*z).

 Lemma mult_plus_distr_l : forall x y z, x*(y+z)=x*y+x*z.

 Lemma mult_0_l : forall x, 0*x = 0.


 Definition plus_opp_r := opp_def.

 Lemma plus_opp_l : forall x, -x + x = 0.

 Lemma mult_opp_comm : forall x y, - x * y = x * - y.

 Lemma opp_eq_mult_neg_1 : forall x, -x = x * -(1).

 Lemma opp_involutive : forall x, -(-x) = x.

 Lemma opp_plus_distr : forall x y, -(x+y) = -x + -y.

 Lemma opp_mult_distr_r : forall x y, -(x*y) = x * -y.

 Lemma egal_left : forall n m, n=m -> n+-m = 0.

 Lemma ne_left_2 : forall x y : int, x<>y -> 0<>(x + - y).


 Lemma red_factor0 : forall n, n = n*1.

 Lemma red_factor1 : forall n, n+n = n*2.

 Lemma red_factor2 : forall n m, n + n*m = n * (1+m).

 Lemma red_factor3 : forall n m, n*m + n = n*(1+m).

 Lemma red_factor4 : forall n m p, n*m + n*p = n*(m+p).

 Lemma red_factor5 : forall n m , n * 0 + m = m.

 Definition red_factor6 := plus_0_r_reverse.


 Hint Rewrite mult_plus_distr_l mult_plus_distr_r mult_assoc : int.
 Hint Rewrite <- plus_assoc : int.

 Lemma OMEGA10 :
  forall v c1 c2 l1 l2 k1 k2 : int,
  (v * c1 + l1) * k1 + (v * c2 + l2) * k2 =
  v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2).

 Lemma OMEGA11 :
  forall v1 c1 l1 l2 k1 : int,
  (v1 * c1 + l1) * k1 + l2 = v1 * (c1 * k1) + (l1 * k1 + l2).

 Lemma OMEGA12 :
  forall v2 c2 l1 l2 k2 : int,
  l1 + (v2 * c2 + l2) * k2 = v2 * (c2 * k2) + (l1 + l2 * k2).

 Lemma OMEGA13 :
  forall v l1 l2 x : int,
  v * -x + l1 + (v * x + l2) = l1 + l2.

 Lemma OMEGA15 :
  forall v c1 c2 l1 l2 k2 : int,
  v * c1 + l1 + (v * c2 + l2) * k2 = v * (c1 + c2 * k2) + (l1 + l2 * k2).

 Lemma OMEGA16 : forall v c l k : int, (v * c + l) * k = v * (c * k) + l * k.

 Lemma sum1 : forall a b c d : int, 0 = a -> 0 = b -> 0 = a * c + b * d.


 Lemma lt_irrefl : forall n, ~ n<n.

 Lemma lt_antisym : forall n m, n<m -> m<n -> False.

 Lemma lt_le_weak : forall n m, n<m -> n<=m.

 Lemma le_refl : forall n, n<=n.

 Lemma le_antisym : forall n m, n<=m -> m<=n -> n=m.

 Lemma lt_eq_lt_dec : forall n m, { n<m }+{ n=m }+{ m<n }.

 Lemma lt_dec : forall n m: int, { n<m } + { ~n<m }.

 Lemma lt_le_iff : forall n m, (n<m) <-> ~(m<=n).

 Lemma le_dec : forall n m: int, { n<=m } + { ~n<=m }.

 Lemma le_lt_dec : forall n m, { n<=m } + { m<n }.

 Definition beq i j := match compare i j with Eq => true | _ => false end.

 Lemma beq_iff : forall i j, beq i j = true <-> i=j.

 Lemma beq_true : forall i j, beq i j = true -> i=j.

 Lemma beq_false : forall i j, beq i j = false -> i<>j.

 Lemma eq_dec : forall n m:int, { n=m } + { n<>m }.

 Definition bgt i j := match compare i j with Gt => true | _ => false end.

 Lemma bgt_iff : forall i j, bgt i j = true <-> i>j.

 Lemma bgt_true : forall i j, bgt i j = true -> i>j.

 Lemma bgt_false : forall i j, bgt i j = false -> i<=j.

 Lemma le_is_lt_or_eq : forall n m, n<=m -> { n<m } + { n=m }.

 Lemma le_neq_lt : forall n m, n<=m -> n<>m -> n<m.

 Lemma le_trans : forall n m p, n<=m -> m<=p -> n<=p.


 Lemma le_0_neg : forall n, 0 <= n <-> -n <= 0.

 Lemma le_0_neg' : forall n, n <= 0 <-> 0 <= -n.

 Lemma plus_le_reg_r : forall n m p, n + p <= m + p -> n <= m.

 Lemma plus_le_lt_compat : forall n m p q, n<=m -> p<q -> n+p<m+q.

 Lemma plus_lt_compat : forall n m p q, n<m -> p<q -> n+p<m+q.

 Lemma opp_lt_compat : forall n m, n<m -> -m < -n.

 Lemma lt_0_neg : forall n, 0 < n <-> -n < 0.

 Lemma lt_0_neg' : forall n, n < 0 <-> 0 < -n.

 Lemma mult_lt_0_compat : forall n m, 0 < n -> 0 < m -> 0 < n*m.

 Lemma mult_integral : forall n m, n * m = 0 -> n = 0 \/ m = 0.

 Lemma mult_le_compat :
   forall i j k l, i<=j -> k<=l -> 0<=i -> 0<=k -> i*k<=j*l.

 Lemma sum5 :
 forall a b c d : int, c <> 0 -> 0 <> a -> 0 = b -> 0 <> a * c + b * d.

 Lemma one_neq_zero : 1 <> 0.

 Lemma minus_one_neq_zero : -(1) <> 0.

 Lemma le_left : forall n m, n <= m -> 0 <= m + - n.

 Lemma OMEGA2 : forall x y, 0 <= x -> 0 <= y -> 0 <= x + y.

 Lemma OMEGA8 : forall x y, 0 <= x -> 0 <= y -> x = - y -> x = 0.

 Lemma sum2 :
 forall a b c d : int, 0 <= d -> 0 = a -> 0 <= b -> 0 <= a * c + b * d.

 Lemma sum3 :
 forall a b c d : int,
  0 <= c -> 0 <= d -> 0 <= a -> 0 <= b -> 0 <= a * c + b * d.

 Lemma sum4 : forall k : int, k>0 -> 0 <= k.


 Lemma lt_left : forall n m, n < m -> 0 <= m + -(1) + - n.

 Lemma lt_left_inv : forall x y, 0 <= y + -(1) + - x -> x < y.

 Lemma OMEGA4 : forall x y z, x > 0 -> y > x -> z * y + x <> 0.

 Lemma OMEGA19 : forall x, x<>0 -> 0 <= x + -(1) \/ 0 <= x * -(1) + -(1).

 Lemma mult_le_approx :
  forall n m p, n > 0 -> n > p -> 0 <= m * n + p -> 0 <= m.


 Lemma dec_eq : forall i j:int, decidable (i=j).

 Lemma dec_ne : forall i j:int, decidable (i<>j).

 Lemma dec_le : forall i j:int, decidable (i<=j).

 Lemma dec_lt : forall i j:int, decidable (i<j).

 Lemma dec_ge : forall i j:int, decidable (i>=j).

 Lemma dec_gt : forall i j:int, decidable (i>j).

End IntProperties.

Module IntOmega (I:Int).
Import I.
Module IP:=IntProperties(I).
Import IP.


Inductive term : Set :=
  | Tint : int -> term
  | Tplus : term -> term -> term
  | Tmult : term -> term -> term
  | Tminus : term -> term -> term
  | Topp : term -> term
  | Tvar : nat -> term.

Delimit Scope romega_scope with term.

Infix "+" := Tplus : romega_scope.
Infix "*" := Tmult : romega_scope.
Infix "-" := Tminus : romega_scope.
Notation "- x" := (Topp x) : romega_scope.
Notation "[ x ]" := (Tvar x) (at level 0) : romega_scope.



Inductive proposition : Set :=
  | EqTerm : term -> term -> proposition
  | LeqTerm : term -> term -> proposition
  | TrueTerm : proposition
  | FalseTerm : proposition
  | Tnot : proposition -> proposition
  | GeqTerm : term -> term -> proposition
  | GtTerm : term -> term -> proposition
  | LtTerm : term -> term -> proposition
  | NeqTerm : term -> term -> proposition
  | Tor : proposition -> proposition -> proposition
  | Tand : proposition -> proposition -> proposition
  | Timp : proposition -> proposition -> proposition
  | Tprop : nat -> proposition.

Notation hyps := (list proposition).

Notation lhyps := (list hyps).

Notation singleton := (fun a : hyps => a :: nil).

Definition absurd := FalseTerm :: nil.


Inductive t_fusion : Set :=
  | F_equal : t_fusion
  | F_cancel : t_fusion
  | F_left : t_fusion
  | F_right : t_fusion.

Inductive step : Set :=
  
  | C_DO_BOTH : step -> step -> step
  
  | C_LEFT : step -> step
  
  | C_RIGHT : step -> step
  
  | C_SEQ : step -> step -> step
  
  | C_NOP : step
  
  | C_OPP_PLUS : step
  | C_OPP_OPP : step
  | C_OPP_MULT_R : step
  | C_OPP_ONE : step
  
  | C_REDUCE : step
  | C_MULT_PLUS_DISTR : step
  | C_MULT_OPP_LEFT : step
  | C_MULT_ASSOC_R : step
  | C_PLUS_ASSOC_R : step
  | C_PLUS_ASSOC_L : step
  | C_PLUS_PERMUTE : step
  | C_PLUS_COMM : step
  | C_RED0 : step
  | C_RED1 : step
  | C_RED2 : step
  | C_RED3 : step
  | C_RED4 : step
  | C_RED5 : step
  | C_RED6 : step
  | C_MULT_ASSOC_REDUCED : step
  | C_MINUS : step
  | C_MULT_COMM : step.


Inductive t_omega : Set :=
  
  | O_CONSTANT_NOT_NUL : nat -> t_omega
  | O_CONSTANT_NEG : nat -> t_omega
  
  | O_DIV_APPROX : int -> int -> term -> nat -> t_omega -> nat -> t_omega
  
  | O_NOT_EXACT_DIVIDE : int -> int -> term -> nat -> nat -> t_omega
  
  | O_EXACT_DIVIDE : int -> term -> nat -> t_omega -> nat -> t_omega
  | O_SUM : int -> nat -> int -> nat -> list t_fusion -> t_omega -> t_omega
  | O_CONTRADICTION : nat -> nat -> nat -> t_omega
  | O_MERGE_EQ : nat -> nat -> nat -> t_omega -> t_omega
  | O_SPLIT_INEQ : nat -> nat -> t_omega -> t_omega -> t_omega
  | O_CONSTANT_NUL : nat -> t_omega
  | O_NEGATE_CONTRADICT : nat -> nat -> t_omega
  | O_NEGATE_CONTRADICT_INV : nat -> nat -> nat -> t_omega
  | O_STATE : int -> step -> nat -> nat -> t_omega -> t_omega.


Inductive p_step : Set :=
  | P_LEFT : p_step -> p_step
  | P_RIGHT : p_step -> p_step
  | P_INVERT : step -> p_step
  | P_STEP : step -> p_step
  | P_NOP : p_step.


Inductive h_step : Set :=
    pair_step : nat -> p_step -> h_step.


Inductive direction : Set :=
  | D_left : direction
  | D_right : direction
  | D_mono : direction.


Inductive e_step : Set :=
  | E_SPLIT : nat -> list direction -> e_step -> e_step -> e_step
  | E_EXTRACT : nat -> list direction -> e_step -> e_step
  | E_SOLVE : t_omega -> e_step.



Open Scope romega_scope.

Fixpoint eq_term (t1 t2 : term) {struct t2} : bool :=
  match t1, t2 with
  | Tint st1, Tint st2 => beq st1 st2
  | (st11 + st12), (st21 + st22) => eq_term st11 st21 && eq_term st12 st22
  | (st11 * st12), (st21 * st22) => eq_term st11 st21 && eq_term st12 st22
  | (st11 - st12), (st21 - st22) => eq_term st11 st21 && eq_term st12 st22
  | (- st1), (- st2) => eq_term st1 st2
  | [st1], [st2] => beq_nat st1 st2
  | _, _ => false
  end.

Close Scope romega_scope.

Theorem eq_term_true : forall t1 t2 : term, eq_term t1 t2 = true -> t1 = t2.

Ltac trivial_case := unfold not in |- *; intros; discriminate.

Theorem eq_term_false :
 forall t1 t2 : term, eq_term t1 t2 = false -> t1 <> t2.



Ltac elim_eq_term t1 t2 :=
  pattern (eq_term t1 t2) in |- *; apply bool_eq_ind; intro Aux;
   [ generalize (eq_term_true t1 t2 Aux); clear Aux
   | generalize (eq_term_false t1 t2 Aux); clear Aux ].

Ltac elim_beq t1 t2 :=
  pattern (beq t1 t2) in |- *; apply bool_eq_ind; intro Aux;
   [ generalize (beq_true t1 t2 Aux); clear Aux
   | generalize (beq_false t1 t2 Aux); clear Aux ].

Ltac elim_bgt t1 t2 :=
  pattern (bgt t1 t2) in |- *; apply bool_eq_ind; intro Aux;
  [ generalize (bgt_true t1 t2 Aux); clear Aux
  | generalize (bgt_false t1 t2 Aux); clear Aux ].


Fixpoint interp_term (env : list int) (t : term) {struct t} : int :=
  match t with
  | Tint x => x
  | (t1 + t2)%term => interp_term env t1 + interp_term env t2
  | (t1 * t2)%term => interp_term env t1 * interp_term env t2
  | (t1 - t2)%term => interp_term env t1 - interp_term env t2
  | (- t)%term => - interp_term env t
  | [n]%term => nth n env 0
  end.


Fixpoint interp_proposition (envp : list Prop) (env : list int)
 (p : proposition) {struct p} : Prop :=
  match p with
  | EqTerm t1 t2 => interp_term env t1 = interp_term env t2
  | LeqTerm t1 t2 => interp_term env t1 <= interp_term env t2
  | TrueTerm => True
  | FalseTerm => False
  | Tnot p' => ~ interp_proposition envp env p'
  | GeqTerm t1 t2 => interp_term env t1 >= interp_term env t2
  | GtTerm t1 t2 => interp_term env t1 > interp_term env t2
  | LtTerm t1 t2 => interp_term env t1 < interp_term env t2
  | NeqTerm t1 t2 => (interp_term env t1)<>(interp_term env t2)
  | Tor p1 p2 =>
      interp_proposition envp env p1 \/ interp_proposition envp env p2
  | Tand p1 p2 =>
      interp_proposition envp env p1 /\ interp_proposition envp env p2
  | Timp p1 p2 =>
      interp_proposition envp env p1 -> interp_proposition envp env p2
  | Tprop n => nth n envp True
  end.


Fixpoint interp_hyps (envp : list Prop) (env : list int)
 (l : hyps) {struct l} : Prop :=
  match l with
  | nil => True
  | p' :: l' => interp_proposition envp env p' /\ interp_hyps envp env l'
  end.


Fixpoint interp_goal_concl (c : proposition) (envp : list Prop)
 (env : list int) (l : hyps) {struct l} : Prop :=
  match l with
  | nil => interp_proposition envp env c
  | p' :: l' =>
      interp_proposition envp env p' -> interp_goal_concl c envp env l'
  end.

Notation interp_goal := (interp_goal_concl FalseTerm).


Theorem goal_to_hyps :
 forall (envp : list Prop) (env : list int) (l : hyps),
 (interp_hyps envp env l -> False) -> interp_goal envp env l.

Theorem hyps_to_goal :
 forall (envp : list Prop) (env : list int) (l : hyps),
 interp_goal envp env l -> interp_hyps envp env l -> False.


Definition term_stable (f : term -> term) :=
  forall (e : list int) (t : term), interp_term e t = interp_term e (f t).


Definition valid1 (f : proposition -> proposition) :=
  forall (ep : list Prop) (e : list int) (p1 : proposition),
  interp_proposition ep e p1 -> interp_proposition ep e (f p1).

Definition valid2 (f : proposition -> proposition -> proposition) :=
  forall (ep : list Prop) (e : list int) (p1 p2 : proposition),
  interp_proposition ep e p1 ->
  interp_proposition ep e p2 -> interp_proposition ep e (f p1 p2).


Definition valid_hyps (f : hyps -> hyps) :=
  forall (ep : list Prop) (e : list int) (lp : hyps),
  interp_hyps ep e lp -> interp_hyps ep e (f lp).


Theorem valid_goal :
  forall (ep : list Prop) (env : list int) (l : hyps) (a : hyps -> hyps),
  valid_hyps a -> interp_goal ep env (a l) -> interp_goal ep env l.


Fixpoint interp_list_hyps (envp : list Prop) (env : list int)
 (l : lhyps) {struct l} : Prop :=
  match l with
  | nil => False
  | h :: l' => interp_hyps envp env h \/ interp_list_hyps envp env l'
  end.

Fixpoint interp_list_goal (envp : list Prop) (env : list int)
 (l : lhyps) {struct l} : Prop :=
  match l with
  | nil => True
  | h :: l' => interp_goal envp env h /\ interp_list_goal envp env l'
  end.

Theorem list_goal_to_hyps :
 forall (envp : list Prop) (env : list int) (l : lhyps),
 (interp_list_hyps envp env l -> False) -> interp_list_goal envp env l.

Theorem list_hyps_to_goal :
 forall (envp : list Prop) (env : list int) (l : lhyps),
 interp_list_goal envp env l -> interp_list_hyps envp env l -> False.

Definition valid_list_hyps (f : hyps -> lhyps) :=
  forall (ep : list Prop) (e : list int) (lp : hyps),
  interp_hyps ep e lp -> interp_list_hyps ep e (f lp).

Definition valid_list_goal (f : hyps -> lhyps) :=
  forall (ep : list Prop) (e : list int) (lp : hyps),
  interp_list_goal ep e (f lp) -> interp_goal ep e lp.

Theorem goal_valid :
 forall f : hyps -> lhyps, valid_list_hyps f -> valid_list_goal f.

Theorem append_valid :
 forall (ep : list Prop) (e : list int) (l1 l2 : lhyps),
 interp_list_hyps ep e l1 \/ interp_list_hyps ep e l2 ->
 interp_list_hyps ep e (l1 ++ l2).


Definition nth_hyps (n : nat) (l : hyps) := nth n l TrueTerm.

Theorem nth_valid :
 forall (ep : list Prop) (e : list int) (i : nat) (l : hyps),
 interp_hyps ep e l -> interp_proposition ep e (nth_hyps i l).

Definition apply_oper_2 (i j : nat)
  (f : proposition -> proposition -> proposition) (l : hyps) :=
  f (nth_hyps i l) (nth_hyps j l) :: l.

Theorem apply_oper_2_valid :
 forall (i j : nat) (f : proposition -> proposition -> proposition),
 valid2 f -> valid_hyps (apply_oper_2 i j f).


Fixpoint apply_oper_1 (i : nat) (f : proposition -> proposition)
 (l : hyps) {struct i} : hyps :=
  match l with
  | nil => nil (A:=proposition)
  | p :: l' =>
      match i with
      | O => f p :: l'
      | S j => p :: apply_oper_1 j f l'
      end
  end.

Theorem apply_oper_1_valid :
 forall (i : nat) (f : proposition -> proposition),
 valid1 f -> valid_hyps (apply_oper_1 i f).


Definition apply_left (f : term -> term) (t : term) :=
  match t with
  | (x + y)%term => (f x + y)%term
  | (x * y)%term => (f x * y)%term
  | (- x)%term => (- f x)%term
  | x => x
  end.

Definition apply_right (f : term -> term) (t : term) :=
  match t with
  | (x + y)%term => (x + f y)%term
  | (x * y)%term => (x * f y)%term
  | x => x
  end.

Definition apply_both (f g : term -> term) (t : term) :=
  match t with
  | (x + y)%term => (f x + g y)%term
  | (x * y)%term => (f x * g y)%term
  | x => x
  end.


Theorem apply_left_stable :
 forall f : term -> term, term_stable f -> term_stable (apply_left f).

Theorem apply_right_stable :
 forall f : term -> term, term_stable f -> term_stable (apply_right f).

Theorem apply_both_stable :
 forall f g : term -> term,
 term_stable f -> term_stable g -> term_stable (apply_both f g).

Theorem compose_term_stable :
 forall f g : term -> term,
 term_stable f -> term_stable g -> term_stable (fun t : term => f (g t)).



Ltac loop t :=
  match t with
  
  | (?X1 = ?X2) => loop X1 || loop X2
  | (_ -> ?X1) => loop X1
  
  | (interp_hyps _ _ ?X1) => loop X1
  | (interp_list_hyps _ _ ?X1) => loop X1
  | (interp_proposition _ _ ?X1) => loop X1
  | (interp_term _ ?X1) => loop X1
  
  | (EqTerm ?X1 ?X2) => loop X1 || loop X2
  | (LeqTerm ?X1 ?X2) => loop X1 || loop X2
  
  | (?X1 + ?X2)%term => loop X1 || loop X2
  | (?X1 - ?X2)%term => loop X1 || loop X2
  | (?X1 * ?X2)%term => loop X1 || loop X2
  | (- ?X1)%term => loop X1
  | (Tint ?X1) => loop X1
  
  | match ?X1 with
    | EqTerm x x0 => _
    | LeqTerm x x0 => _
    | TrueTerm => _
    | FalseTerm => _
    | Tnot x => _
    | GeqTerm x x0 => _
    | GtTerm x x0 => _
    | LtTerm x x0 => _
    | NeqTerm x x0 => _
    | Tor x x0 => _
    | Tand x x0 => _
    | Timp x x0 => _
    | Tprop x => _
    end => destruct X1; auto; Simplify
  | match ?X1 with
    | Tint x => _
    | (x + x0)%term => _
    | (x * x0)%term => _
    | (x - x0)%term => _
    | (- x)%term => _
    | [x]%term => _
    end => destruct X1; auto; Simplify
  | (if beq ?X1 ?X2 then _ else _) =>
      let H := fresh "H" in
      elim_beq X1 X2; intro H; try (rewrite H in *; clear H);
       simpl in |- *; auto; Simplify
  | (if bgt ?X1 ?X2 then _ else _) =>
      let H := fresh "H" in
      elim_bgt X1 X2; intro H; simpl in |- *; auto; Simplify
  | (if eq_term ?X1 ?X2 then _ else _) =>
      let H := fresh "H" in
      elim_eq_term X1 X2; intro H; try (rewrite H in *; clear H);
       simpl in |- *; auto; Simplify
  | (if _ && _ then _ else _) => rewrite andb_if; Simplify
  | (if negb _ then _ else _) => rewrite negb_if; Simplify
  | _ => fail
  end

with Simplify := match goal with
  | |- ?X1 => try loop X1
  | _ => idtac
  end.

Ltac prove_stable x th :=
  match constr:x with
  | ?X1 =>
      unfold term_stable, X1 in |- *; intros; Simplify; simpl in |- *;
       apply th
  end.

Definition Tplus_assoc_l (t : term) :=
  match t with
  | (n + (m + p))%term => (n + m + p)%term
  | _ => t
  end.

Theorem Tplus_assoc_l_stable : term_stable Tplus_assoc_l.

Definition Tplus_assoc_r (t : term) :=
  match t with
  | (n + m + p)%term => (n + (m + p))%term
  | _ => t
  end.

Theorem Tplus_assoc_r_stable : term_stable Tplus_assoc_r.

Definition Tmult_assoc_r (t : term) :=
  match t with
  | (n * m * p)%term => (n * (m * p))%term
  | _ => t
  end.

Theorem Tmult_assoc_r_stable : term_stable Tmult_assoc_r.

Definition Tplus_permute (t : term) :=
  match t with
  | (n + (m + p))%term => (m + (n + p))%term
  | _ => t
  end.

Theorem Tplus_permute_stable : term_stable Tplus_permute.

Definition Tplus_comm (t : term) :=
  match t with
  | (x + y)%term => (y + x)%term
  | _ => t
  end.

Theorem Tplus_comm_stable : term_stable Tplus_comm.

Definition Tmult_comm (t : term) :=
  match t with
  | (x * y)%term => (y * x)%term
  | _ => t
  end.

Theorem Tmult_comm_stable : term_stable Tmult_comm.

Definition T_OMEGA10 (t : term) :=
  match t with
  | ((v * Tint c1 + l1) * Tint k1 + (v' * Tint c2 + l2) * Tint k2)%term =>
      if eq_term v v'
      then (v * Tint (c1 * k1 + c2 * k2)%I + (l1 * Tint k1 + l2 * Tint k2))%term
      else t
  | _ => t
  end.

Theorem T_OMEGA10_stable : term_stable T_OMEGA10.

Definition T_OMEGA11 (t : term) :=
  match t with
  | ((v1 * Tint c1 + l1) * Tint k1 + l2)%term =>
      (v1 * Tint (c1 * k1) + (l1 * Tint k1 + l2))%term
  | _ => t
  end.

Theorem T_OMEGA11_stable : term_stable T_OMEGA11.

Definition T_OMEGA12 (t : term) :=
  match t with
  | (l1 + (v2 * Tint c2 + l2) * Tint k2)%term =>
      (v2 * Tint (c2 * k2) + (l1 + l2 * Tint k2))%term
  | _ => t
  end.

Theorem T_OMEGA12_stable : term_stable T_OMEGA12.

Definition T_OMEGA13 (t : term) :=
  match t with
  | (v * Tint x + l1 + (v' * Tint x' + l2))%term =>
      if eq_term v v' && beq x (-x')
      then (l1+l2)%term
      else t
  | _ => t
  end.

Theorem T_OMEGA13_stable : term_stable T_OMEGA13.

Definition T_OMEGA15 (t : term) :=
  match t with
  | (v * Tint c1 + l1 + (v' * Tint c2 + l2) * Tint k2)%term =>
      if eq_term v v'
      then (v * Tint (c1 + c2 * k2)%I + (l1 + l2 * Tint k2))%term
      else t
  | _ => t
  end.

Theorem T_OMEGA15_stable : term_stable T_OMEGA15.

Definition T_OMEGA16 (t : term) :=
  match t with
  | ((v * Tint c + l) * Tint k)%term => (v * Tint (c * k) + l * Tint k)%term
  | _ => t
  end.

Theorem T_OMEGA16_stable : term_stable T_OMEGA16.

Definition Tred_factor5 (t : term) :=
  match t with
  | (x * Tint c + y)%term => if beq c 0 then y else t
  | _ => t
  end.

Theorem Tred_factor5_stable : term_stable Tred_factor5.

Definition Topp_plus (t : term) :=
  match t with
  | (- (x + y))%term => (- x + - y)%term
  | _ => t
  end.

Theorem Topp_plus_stable : term_stable Topp_plus.

Definition Topp_opp (t : term) :=
  match t with
  | (- - x)%term => x
  | _ => t
  end.

Theorem Topp_opp_stable : term_stable Topp_opp.

Definition Topp_mult_r (t : term) :=
  match t with
  | (- (x * Tint k))%term => (x * Tint (- k))%term
  | _ => t
  end.

Theorem Topp_mult_r_stable : term_stable Topp_mult_r.

Definition Topp_one (t : term) :=
  match t with
  | (- x)%term => (x * Tint (-(1)))%term
  | _ => t
  end.

Theorem Topp_one_stable : term_stable Topp_one.

Definition Tmult_plus_distr (t : term) :=
  match t with
  | ((n + m) * p)%term => (n * p + m * p)%term
  | _ => t
  end.

Theorem Tmult_plus_distr_stable : term_stable Tmult_plus_distr.

Definition Tmult_opp_left (t : term) :=
  match t with
  | (- x * Tint y)%term => (x * Tint (- y))%term
  | _ => t
  end.

Theorem Tmult_opp_left_stable : term_stable Tmult_opp_left.

Definition Tmult_assoc_reduced (t : term) :=
  match t with
  | (n * Tint m * Tint p)%term => (n * Tint (m * p))%term
  | _ => t
  end.

Theorem Tmult_assoc_reduced_stable : term_stable Tmult_assoc_reduced.

Definition Tred_factor0 (t : term) := (t * Tint 1)%term.

Theorem Tred_factor0_stable : term_stable Tred_factor0.

Definition Tred_factor1 (t : term) :=
  match t with
  | (x + y)%term =>
      if eq_term x y
      then (x * Tint 2)%term
      else t
  | _ => t
  end.

Theorem Tred_factor1_stable : term_stable Tred_factor1.

Definition Tred_factor2 (t : term) :=
  match t with
  | (x + y * Tint k)%term =>
      if eq_term x y
      then (x * Tint (1 + k))%term
      else t
  | _ => t
  end.

Theorem Tred_factor2_stable : term_stable Tred_factor2.

Definition Tred_factor3 (t : term) :=
  match t with
  | (x * Tint k + y)%term =>
      if eq_term x y
      then (x * Tint (1 + k))%term
      else t
  | _ => t
  end.

Theorem Tred_factor3_stable : term_stable Tred_factor3.

Definition Tred_factor4 (t : term) :=
  match t with
  | (x * Tint k1 + y * Tint k2)%term =>
      if eq_term x y
      then (x * Tint (k1 + k2))%term
      else t
  | _ => t
  end.

Theorem Tred_factor4_stable : term_stable Tred_factor4.

Definition Tred_factor6 (t : term) := (t + Tint 0)%term.

Theorem Tred_factor6_stable : term_stable Tred_factor6.

Definition Tminus_def (t : term) :=
  match t with
  | (x - y)%term => (x + - y)%term
  | _ => t
  end.

Theorem Tminus_def_stable : term_stable Tminus_def.



Fixpoint reduce (t : term) : term :=
  match t with
  | (x + y)%term =>
      match reduce x with
      | Tint x' =>
          match reduce y with
          | Tint y' => Tint (x' + y')
          | y' => (Tint x' + y')%term
          end
      | x' => (x' + reduce y)%term
      end
  | (x * y)%term =>
      match reduce x with
      | Tint x' =>
          match reduce y with
          | Tint y' => Tint (x' * y')
          | y' => (Tint x' * y')%term
          end
      | x' => (x' * reduce y)%term
      end
  | (x - y)%term =>
      match reduce x with
      | Tint x' =>
          match reduce y with
          | Tint y' => Tint (x' - y')
          | y' => (Tint x' - y')%term
          end
      | x' => (x' - reduce y)%term
      end
  | (- x)%term =>
      match reduce x with
      | Tint x' => Tint (- x')
      | x' => (- x')%term
      end
  | _ => t
  end.

Theorem reduce_stable : term_stable reduce.


Fixpoint fusion (trace : list t_fusion) (t : term) {struct trace} : term :=
  match trace with
  | nil => reduce t
  | step :: trace' =>
      match step with
      | F_equal => apply_right (fusion trace') (T_OMEGA10 t)
      | F_cancel => fusion trace' (Tred_factor5 (T_OMEGA10 t))
      | F_left => apply_right (fusion trace') (T_OMEGA11 t)
      | F_right => apply_right (fusion trace') (T_OMEGA12 t)
      end
  end.

Theorem fusion_stable : forall t : list t_fusion, term_stable (fusion t).


Definition fusion_right (trace : list t_fusion) (t : term) : term :=
  match trace with
  | nil => reduce t
  | step :: trace' =>
      match step with
      | F_equal => apply_right (fusion trace') (T_OMEGA15 t)
      | F_cancel => fusion trace' (Tred_factor5 (T_OMEGA15 t))
      | F_left => apply_right (fusion trace') (Tplus_assoc_r t)
      | F_right => apply_right (fusion trace') (T_OMEGA12 t)
      end
  end.


Fixpoint fusion_cancel (trace : nat) (t : term) {struct trace} : term :=
  match trace with
  | O => reduce t
  | S trace' => fusion_cancel trace' (T_OMEGA13 t)
  end.

Theorem fusion_cancel_stable : forall t : nat, term_stable (fusion_cancel t).


Fixpoint scalar_norm_add (trace : nat) (t : term) {struct trace} : term :=
  match trace with
  | O => reduce t
  | S trace' => apply_right (scalar_norm_add trace') (T_OMEGA11 t)
  end.

Theorem scalar_norm_add_stable :
 forall t : nat, term_stable (scalar_norm_add t).

Fixpoint scalar_norm (trace : nat) (t : term) {struct trace} : term :=
  match trace with
  | O => reduce t
  | S trace' => apply_right (scalar_norm trace') (T_OMEGA16 t)
  end.

Theorem scalar_norm_stable : forall t : nat, term_stable (scalar_norm t).

Fixpoint add_norm (trace : nat) (t : term) {struct trace} : term :=
  match trace with
  | O => reduce t
  | S trace' => apply_right (add_norm trace') (Tplus_assoc_r t)
  end.

Theorem add_norm_stable : forall t : nat, term_stable (add_norm t).


Fixpoint rewrite (s : step) : term -> term :=
  match s with
  | C_DO_BOTH s1 s2 => apply_both (rewrite s1) (rewrite s2)
  | C_LEFT s => apply_left (rewrite s)
  | C_RIGHT s => apply_right (rewrite s)
  | C_SEQ s1 s2 => fun t : term => rewrite s2 (rewrite s1 t)
  | C_NOP => fun t : term => t
  | C_OPP_PLUS => Topp_plus
  | C_OPP_OPP => Topp_opp
  | C_OPP_MULT_R => Topp_mult_r
  | C_OPP_ONE => Topp_one
  | C_REDUCE => reduce
  | C_MULT_PLUS_DISTR => Tmult_plus_distr
  | C_MULT_OPP_LEFT => Tmult_opp_left
  | C_MULT_ASSOC_R => Tmult_assoc_r
  | C_PLUS_ASSOC_R => Tplus_assoc_r
  | C_PLUS_ASSOC_L => Tplus_assoc_l
  | C_PLUS_PERMUTE => Tplus_permute
  | C_PLUS_COMM => Tplus_comm
  | C_RED0 => Tred_factor0
  | C_RED1 => Tred_factor1
  | C_RED2 => Tred_factor2
  | C_RED3 => Tred_factor3
  | C_RED4 => Tred_factor4
  | C_RED5 => Tred_factor5
  | C_RED6 => Tred_factor6
  | C_MULT_ASSOC_REDUCED => Tmult_assoc_reduced
  | C_MINUS => Tminus_def
  | C_MULT_COMM => Tmult_comm
  end.

Theorem rewrite_stable : forall s : step, term_stable (rewrite s).


Definition constant_not_nul (i : nat) (h : hyps) :=
  match nth_hyps i h with
  | EqTerm (Tint Nul) (Tint n) =>
      if beq n Nul then h else absurd
  | _ => h
  end.

Theorem constant_not_nul_valid :
 forall i : nat, valid_hyps (constant_not_nul i).


Definition constant_neg (i : nat) (h : hyps) :=
  match nth_hyps i h with
  | LeqTerm (Tint Nul) (Tint Neg) =>
     if bgt Nul Neg then absurd else h
  | _ => h
  end.

Theorem constant_neg_valid : forall i : nat, valid_hyps (constant_neg i).

Definition not_exact_divide (k1 k2 : int) (body : term)
  (t i : nat) (l : hyps) :=
  match nth_hyps i l with
  | EqTerm (Tint Nul) b =>
      if beq Nul 0 &&
         eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) b &&
         bgt k2 0 &&
         bgt k1 k2
      then absurd
      else l
  | _ => l
  end.

Theorem not_exact_divide_valid :
 forall (k1 k2 : int) (body : term) (t i : nat),
 valid_hyps (not_exact_divide k1 k2 body t i).


Definition contradiction (t i j : nat) (l : hyps) :=
  match nth_hyps i l with
  | LeqTerm (Tint Nul) b1 =>
      match nth_hyps j l with
      | LeqTerm (Tint Nul') b2 =>
          match fusion_cancel t (b1 + b2)%term with
          | Tint k => if beq Nul 0 && beq Nul' 0 && bgt 0 k
                      then absurd
                      else l
          | _ => l
          end
      | _ => l
      end
  | _ => l
  end.

Theorem contradiction_valid :
 forall t i j : nat, valid_hyps (contradiction t i j).


Definition negate_contradict (i1 i2 : nat) (h : hyps) :=
  match nth_hyps i1 h with
  | EqTerm (Tint Nul) b1 =>
      match nth_hyps i2 h with
      | NeqTerm (Tint Nul') b2 =>
          if beq Nul 0 && beq Nul' 0 && eq_term b1 b2
          then absurd
          else h
      | _ => h
      end
  | NeqTerm (Tint Nul) b1 =>
      match nth_hyps i2 h with
      | EqTerm (Tint Nul') b2 =>
          if beq Nul 0 && beq Nul' 0 && eq_term b1 b2
          then absurd
          else h
      | _ => h
      end
  | _ => h
  end.

Definition negate_contradict_inv (t i1 i2 : nat) (h : hyps) :=
  match nth_hyps i1 h with
  | EqTerm (Tint Nul) b1 =>
      match nth_hyps i2 h with
      | NeqTerm (Tint Nul') b2 =>
          if beq Nul 0 && beq Nul' 0 &&
             eq_term b1 (scalar_norm t (b2 * Tint (-(1)))%term)
          then absurd
          else h
      | _ => h
      end
  | NeqTerm (Tint Nul) b1 =>
      match nth_hyps i2 h with
      | EqTerm (Tint Nul') b2 =>
          if beq Nul 0 && beq Nul' 0 &&
             eq_term b1 (scalar_norm t (b2 * Tint (-(1)))%term)
          then absurd
          else h
      | _ => h
      end
  | _ => h
  end.

Theorem negate_contradict_valid :
 forall i j : nat, valid_hyps (negate_contradict i j).

Theorem negate_contradict_inv_valid :
 forall t i j : nat, valid_hyps (negate_contradict_inv t i j).


Definition sum (k1 k2 : int) (trace : list t_fusion)
  (prop1 prop2 : proposition) :=
  match prop1 with
  | EqTerm (Tint Null) b1 =>
      match prop2 with
      | EqTerm (Tint Null') b2 =>
          if beq Null 0 && beq Null' 0
          then EqTerm (Tint 0) (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term)
          else TrueTerm
      | LeqTerm (Tint Null') b2 =>
          if beq Null 0 && beq Null' 0 && bgt k2 0
          then LeqTerm (Tint 0)
                (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term)
          else TrueTerm
      | _ => TrueTerm
      end
  | LeqTerm (Tint Null) b1 =>
      if beq Null 0 && bgt k1 0
      then match prop2 with
          | EqTerm (Tint Null') b2 =>
              if beq Null' 0 then
              LeqTerm (Tint 0)
                (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term)
              else TrueTerm
          | LeqTerm (Tint Null') b2 =>
              if beq Null' 0 && bgt k2 0
              then LeqTerm (Tint 0)
                    (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term)
              else TrueTerm
          | _ => TrueTerm
          end
      else TrueTerm
  | NeqTerm (Tint Null) b1 =>
      match prop2 with
      | EqTerm (Tint Null') b2 =>
          if beq Null 0 && beq Null' 0 && (negb (beq k1 0))
          then NeqTerm (Tint 0)
                 (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term)
          else TrueTerm
      | _ => TrueTerm
      end
  | _ => TrueTerm
  end.

Theorem sum_valid :
 forall (k1 k2 : int) (t : list t_fusion), valid2 (sum k1 k2 t).


Definition exact_divide (k : int) (body : term) (t : nat)
  (prop : proposition) :=
  match prop with
  | EqTerm (Tint Null) b =>
      if beq Null 0 &&
         eq_term (scalar_norm t (body * Tint k)%term) b &&
         negb (beq k 0)
      then EqTerm (Tint 0) body
      else TrueTerm
  | NeqTerm (Tint Null) b =>
      if beq Null 0 &&
         eq_term (scalar_norm t (body * Tint k)%term) b &&
         negb (beq k 0)
      then NeqTerm (Tint 0) body
      else TrueTerm
  | _ => TrueTerm
  end.

Theorem exact_divide_valid :
 forall (k : int) (t : term) (n : nat), valid1 (exact_divide k t n).


Definition divide_and_approx (k1 k2 : int) (body : term)
  (t : nat) (prop : proposition) :=
  match prop with
  | LeqTerm (Tint Null) b =>
      if beq Null 0 &&
         eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) b &&
         bgt k1 0 &&
         bgt k1 k2
      then LeqTerm (Tint 0) body
      else prop
  | _ => prop
  end.

Theorem divide_and_approx_valid :
 forall (k1 k2 : int) (body : term) (t : nat),
 valid1 (divide_and_approx k1 k2 body t).


Definition merge_eq (t : nat) (prop1 prop2 : proposition) :=
  match prop1 with
  | LeqTerm (Tint Null) b1 =>
      match prop2 with
      | LeqTerm (Tint Null') b2 =>
          if beq Null 0 && beq Null' 0 &&
             eq_term b1 (scalar_norm t (b2 * Tint (-(1)))%term)
          then EqTerm (Tint 0) b1
          else TrueTerm
      | _ => TrueTerm
      end
  | _ => TrueTerm
  end.

Theorem merge_eq_valid : forall n : nat, valid2 (merge_eq n).


Definition constant_nul (i : nat) (h : hyps) :=
  match nth_hyps i h with
  | NeqTerm (Tint Null) (Tint Null') =>
      if beq Null Null' then absurd else h
  | _ => h
  end.

Theorem constant_nul_valid : forall i : nat, valid_hyps (constant_nul i).


Definition state (m : int) (s : step) (prop1 prop2 : proposition) :=
  match prop1 with
  | EqTerm (Tint Null) b1 =>
      match prop2 with
      | EqTerm b2 b3 =>
          if beq Null 0
          then EqTerm (Tint 0) (rewrite s (b1 + (- b3 + b2) * Tint m)%term)
          else TrueTerm
      | _ => TrueTerm
      end
  | _ => TrueTerm
  end.

Theorem state_valid : forall (m : int) (s : step), valid2 (state m s).


Definition split_ineq (i t : nat) (f1 f2 : hyps -> lhyps)
  (l : hyps) :=
  match nth_hyps i l with
  | NeqTerm (Tint Null) b1 =>
      if beq Null 0 then
      f1 (LeqTerm (Tint 0) (add_norm t (b1 + Tint (-(1)))%term) :: l) ++
      f2
        (LeqTerm (Tint 0)
           (scalar_norm_add t (b1 * Tint (-(1)) + Tint (-(1)))%term) :: l)
       else l :: nil
  | _ => l :: nil
  end.

Theorem split_ineq_valid :
 forall (i t : nat) (f1 f2 : hyps -> lhyps),
 valid_list_hyps f1 ->
 valid_list_hyps f2 -> valid_list_hyps (split_ineq i t f1 f2).


Fixpoint execute_omega (t : t_omega) (l : hyps) {struct t} : lhyps :=
  match t with
  | O_CONSTANT_NOT_NUL n => singleton (constant_not_nul n l)
  | O_CONSTANT_NEG n => singleton (constant_neg n l)
  | O_DIV_APPROX k1 k2 body t cont n =>
      execute_omega cont (apply_oper_1 n (divide_and_approx k1 k2 body t) l)
  | O_NOT_EXACT_DIVIDE k1 k2 body t i =>
      singleton (not_exact_divide k1 k2 body t i l)
  | O_EXACT_DIVIDE k body t cont n =>
      execute_omega cont (apply_oper_1 n (exact_divide k body t) l)
  | O_SUM k1 i1 k2 i2 t cont =>
      execute_omega cont (apply_oper_2 i1 i2 (sum k1 k2 t) l)
  | O_CONTRADICTION t i j => singleton (contradiction t i j l)
  | O_MERGE_EQ t i1 i2 cont =>
      execute_omega cont (apply_oper_2 i1 i2 (merge_eq t) l)
  | O_SPLIT_INEQ t i cont1 cont2 =>
      split_ineq i t (execute_omega cont1) (execute_omega cont2) l
  | O_CONSTANT_NUL i => singleton (constant_nul i l)
  | O_NEGATE_CONTRADICT i j => singleton (negate_contradict i j l)
  | O_NEGATE_CONTRADICT_INV t i j =>
      singleton (negate_contradict_inv t i j l)
  | O_STATE m s i1 i2 cont =>
      execute_omega cont (apply_oper_2 i1 i2 (state m s) l)
  end.

Theorem omega_valid : forall t : t_omega, valid_list_hyps (execute_omega t).


Definition move_right (s : step) (p : proposition) :=
  match p with
  | EqTerm t1 t2 => EqTerm (Tint 0) (rewrite s (t1 + - t2)%term)
  | LeqTerm t1 t2 => LeqTerm (Tint 0) (rewrite s (t2 + - t1)%term)
  | GeqTerm t1 t2 => LeqTerm (Tint 0) (rewrite s (t1 + - t2)%term)
  | LtTerm t1 t2 => LeqTerm (Tint 0) (rewrite s (t2 + Tint (-(1)) + - t1)%term)
  | GtTerm t1 t2 => LeqTerm (Tint 0) (rewrite s (t1 + Tint (-(1)) + - t2)%term)
  | NeqTerm t1 t2 => NeqTerm (Tint 0) (rewrite s (t1 + - t2)%term)
  | p => p
  end.

Theorem move_right_valid : forall s : step, valid1 (move_right s).

Definition do_normalize (i : nat) (s : step) := apply_oper_1 i (move_right s).

Theorem do_normalize_valid :
 forall (i : nat) (s : step), valid_hyps (do_normalize i s).

Fixpoint do_normalize_list (l : list step) (i : nat)
 (h : hyps) {struct l} : hyps :=
  match l with
  | s :: l' => do_normalize_list l' (S i) (do_normalize i s h)
  | nil => h
  end.

Theorem do_normalize_list_valid :
 forall (l : list step) (i : nat), valid_hyps (do_normalize_list l i).

Theorem normalize_goal :
 forall (s : list step) (ep : list Prop) (env : list int) (l : hyps),
 interp_goal ep env (do_normalize_list s 0 l) -> interp_goal ep env l.


Theorem execute_goal :
 forall (t : t_omega) (ep : list Prop) (env : list int) (l : hyps),
 interp_list_goal ep env (execute_omega t l) -> interp_goal ep env l.

Theorem append_goal :
 forall (ep : list Prop) (e : list int) (l1 l2 : lhyps),
 interp_list_goal ep e l1 /\ interp_list_goal ep e l2 ->
 interp_list_goal ep e (l1 ++ l2).


Fixpoint decidability (p : proposition) : bool :=
  match p with
  | EqTerm _ _ => true
  | LeqTerm _ _ => true
  | GeqTerm _ _ => true
  | GtTerm _ _ => true
  | LtTerm _ _ => true
  | NeqTerm _ _ => true
  | FalseTerm => true
  | TrueTerm => true
  | Tnot t => decidability t
  | Tand t1 t2 => decidability t1 && decidability t2
  | Timp t1 t2 => decidability t1 && decidability t2
  | Tor t1 t2 => decidability t1 && decidability t2
  | Tprop _ => false
  end.

Theorem decidable_correct :
 forall (ep : list Prop) (e : list int) (p : proposition),
 decidability p = true -> decidable (interp_proposition ep e p).


Fixpoint interp_full_goal (envp : list Prop) (env : list int)
 (c : proposition) (l : hyps) {struct l} : Prop :=
  match l with
  | nil => interp_proposition envp env c
  | p' :: l' =>
      interp_proposition envp env p' -> interp_full_goal envp env c l'
  end.

Definition interp_full (ep : list Prop) (e : list int)
  (lc : hyps * proposition) : Prop :=
  match lc with
  | (l, c) => interp_full_goal ep e c l
  end.


Theorem interp_full_false :
 forall (ep : list Prop) (e : list int) (l : hyps) (c : proposition),
 (interp_hyps ep e l -> interp_proposition ep e c) -> interp_full ep e (l, c).


Definition to_contradict (lc : hyps * proposition) :=
  match lc with
  | (l, c) => if decidability c then Tnot c :: l else l
  end.


Theorem to_contradict_valid :
 forall (ep : list Prop) (e : list int) (lc : hyps * proposition),
 interp_goal ep e (to_contradict lc) -> interp_full ep e lc.


Fixpoint map_cons (A : Set) (x : A) (l : list (list A)) {struct l} :
 list (list A) :=
  match l with
  | nil => nil
  | l :: ll => (x :: l) :: map_cons A x ll
  end.


Fixpoint destructure_hyps (nn : nat) (ll : hyps) {struct nn} : lhyps :=
  match nn with
  | O => ll :: nil
  | S n =>
      match ll with
      | nil => nil :: nil
      | Tor p1 p2 :: l =>
          destructure_hyps n (p1 :: l) ++ destructure_hyps n (p2 :: l)
      | Tand p1 p2 :: l => destructure_hyps n (p1 :: p2 :: l)
      | Timp p1 p2 :: l =>
          if decidability p1
          then
           destructure_hyps n (Tnot p1 :: l) ++ destructure_hyps n (p2 :: l)
          else map_cons _ (Timp p1 p2) (destructure_hyps n l)
      | Tnot p :: l =>
          match p with
          | Tnot p1 =>
              if decidability p1
              then destructure_hyps n (p1 :: l)
              else map_cons _ (Tnot (Tnot p1)) (destructure_hyps n l)
          | Tor p1 p2 => destructure_hyps n (Tnot p1 :: Tnot p2 :: l)
          | Tand p1 p2 =>
              if decidability p1
              then
               destructure_hyps n (Tnot p1 :: l) ++
               destructure_hyps n (Tnot p2 :: l)
              else map_cons _ (Tnot p) (destructure_hyps n l)
          | _ => map_cons _ (Tnot p) (destructure_hyps n l)
          end
      | x :: l => map_cons _ x (destructure_hyps n l)
      end
  end.

Theorem map_cons_val :
 forall (ep : list Prop) (e : list int) (p : proposition) (l : lhyps),
 interp_proposition ep e p ->
 interp_list_hyps ep e l -> interp_list_hyps ep e (map_cons _ p l).

Hint Resolve map_cons_val append_valid decidable_correct.

Theorem destructure_hyps_valid :
 forall n : nat, valid_list_hyps (destructure_hyps n).

Definition prop_stable (f : proposition -> proposition) :=
  forall (ep : list Prop) (e : list int) (p : proposition),
  interp_proposition ep e p <-> interp_proposition ep e (f p).

Definition p_apply_left (f : proposition -> proposition)
  (p : proposition) :=
  match p with
  | Timp x y => Timp (f x) y
  | Tor x y => Tor (f x) y
  | Tand x y => Tand (f x) y
  | Tnot x => Tnot (f x)
  | x => x
  end.

Theorem p_apply_left_stable :
 forall f : proposition -> proposition,
 prop_stable f -> prop_stable (p_apply_left f).

Definition p_apply_right (f : proposition -> proposition)
  (p : proposition) :=
  match p with
  | Timp x y => Timp x (f y)
  | Tor x y => Tor x (f y)
  | Tand x y => Tand x (f y)
  | Tnot x => Tnot (f x)
  | x => x
  end.

Theorem p_apply_right_stable :
 forall f : proposition -> proposition,
 prop_stable f -> prop_stable (p_apply_right f).

Definition p_invert (f : proposition -> proposition)
  (p : proposition) :=
  match p with
  | EqTerm x y => Tnot (f (NeqTerm x y))
  | LeqTerm x y => Tnot (f (GtTerm x y))
  | GeqTerm x y => Tnot (f (LtTerm x y))
  | GtTerm x y => Tnot (f (LeqTerm x y))
  | LtTerm x y => Tnot (f (GeqTerm x y))
  | NeqTerm x y => Tnot (f (EqTerm x y))
  | x => x
  end.

Theorem p_invert_stable :
 forall f : proposition -> proposition,
 prop_stable f -> prop_stable (p_invert f).

Theorem move_right_stable : forall s : step, prop_stable (move_right s).

Fixpoint p_rewrite (s : p_step) : proposition -> proposition :=
  match s with
  | P_LEFT s => p_apply_left (p_rewrite s)
  | P_RIGHT s => p_apply_right (p_rewrite s)
  | P_STEP s => move_right s
  | P_INVERT s => p_invert (move_right s)
  | P_NOP => fun p : proposition => p
  end.

Theorem p_rewrite_stable : forall s : p_step, prop_stable (p_rewrite s).

Fixpoint normalize_hyps (l : list h_step) (lh : hyps) {struct l} : hyps :=
  match l with
  | nil => lh
  | pair_step i s :: r => normalize_hyps r (apply_oper_1 i (p_rewrite s) lh)
  end.

Theorem normalize_hyps_valid :
 forall l : list h_step, valid_hyps (normalize_hyps l).

Theorem normalize_hyps_goal :
 forall (s : list h_step) (ep : list Prop) (env : list int) (l : hyps),
 interp_goal ep env (normalize_hyps s l) -> interp_goal ep env l.

Fixpoint extract_hyp_pos (s : list direction) (p : proposition) {struct s} :
 proposition :=
  match s with
  | D_left :: l =>
      match p with
      | Tand x y => extract_hyp_pos l x
      | _ => p
      end
  | D_right :: l =>
      match p with
      | Tand x y => extract_hyp_pos l y
      | _ => p
      end
  | D_mono :: l => match p with
                   | Tnot x => extract_hyp_neg l x
                   | _ => p
                   end
  | _ => p
  end

 with extract_hyp_neg (s : list direction) (p : proposition) {struct s} :
 proposition :=
  match s with
  | D_left :: l =>
      match p with
      | Tor x y => extract_hyp_neg l x
      | Timp x y => if decidability x then extract_hyp_pos l x else Tnot p
      | _ => Tnot p
      end
  | D_right :: l =>
      match p with
      | Tor x y => extract_hyp_neg l y
      | Timp x y => extract_hyp_neg l y
      | _ => Tnot p
      end
  | D_mono :: l =>
      match p with
      | Tnot x => if decidability x then extract_hyp_pos l x else Tnot p
      | _ => Tnot p
      end
  | _ =>
      match p with
      | Tnot x => if decidability x then x else Tnot p
      | _ => Tnot p
      end
  end.

Definition co_valid1 (f : proposition -> proposition) :=
  forall (ep : list Prop) (e : list int) (p1 : proposition),
  interp_proposition ep e (Tnot p1) -> interp_proposition ep e (f p1).

Theorem extract_valid :
 forall s : list direction,
 valid1 (extract_hyp_pos s) /\ co_valid1 (extract_hyp_neg s).

Fixpoint decompose_solve (s : e_step) (h : hyps) {struct s} : lhyps :=
  match s with
  | E_SPLIT i dl s1 s2 =>
      match extract_hyp_pos dl (nth_hyps i h) with
      | Tor x y => decompose_solve s1 (x :: h) ++ decompose_solve s2 (y :: h)
      | Tnot (Tand x y) =>
          if decidability x
          then
           decompose_solve s1 (Tnot x :: h) ++
           decompose_solve s2 (Tnot y :: h)
          else h :: nil
      | Timp x y =>
          if decidability x then
            decompose_solve s1 (Tnot x :: h) ++ decompose_solve s2 (y :: h)
          else h::nil
      | _ => h :: nil
      end
  | E_EXTRACT i dl s1 =>
      decompose_solve s1 (extract_hyp_pos dl (nth_hyps i h) :: h)
  | E_SOLVE t => execute_omega t h
  end.

Theorem decompose_solve_valid :
 forall s : e_step, valid_list_goal (decompose_solve s).


Definition valid_lhyps (f : lhyps -> lhyps) :=
  forall (ep : list Prop) (e : list int) (lp : lhyps),
  interp_list_hyps ep e lp -> interp_list_hyps ep e (f lp).

Fixpoint reduce_lhyps (lp : lhyps) : lhyps :=
  match lp with
  | (FalseTerm :: nil) :: lp' => reduce_lhyps lp'
  | x :: lp' => x :: reduce_lhyps lp'
  | nil => nil (A:=hyps)
  end.

Theorem reduce_lhyps_valid : valid_lhyps reduce_lhyps.

Theorem do_reduce_lhyps :
 forall (envp : list Prop) (env : list int) (l : lhyps),
 interp_list_goal envp env (reduce_lhyps l) -> interp_list_goal envp env l.

Definition concl_to_hyp (p : proposition) :=
  if decidability p then Tnot p else TrueTerm.

Definition do_concl_to_hyp :
  forall (envp : list Prop) (env : list int) (c : proposition) (l : hyps),
  interp_goal envp env (concl_to_hyp c :: l) ->
  interp_goal_concl c envp env l.

Definition omega_tactic (t1 : e_step) (t2 : list h_step)
  (c : proposition) (l : hyps) :=
  reduce_lhyps (decompose_solve t1 (normalize_hyps t2 (concl_to_hyp c :: l))).

Theorem do_omega :
 forall (t1 : e_step) (t2 : list h_step) (envp : list Prop)
   (env : list int) (c : proposition) (l : hyps),
 interp_list_goal envp env (omega_tactic t1 t2 c l) ->
 interp_goal_concl c envp env l.

End IntOmega.


Module ZOmega := IntOmega(Z_as_Int).