# 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).