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 t : Set.
Parameter zero : t.
Parameter one : t.
Parameter plus : t -> t -> t.
Parameter opp : t -> t.
Parameter minus : t -> t -> t.
Parameter mult : t -> t -> t.
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 t 0 1 plus mult minus opp (@eq t).
Parameter le : t -> t -> Prop.
Parameter lt : t -> t -> Prop.
Parameter ge : t -> t -> Prop.
Parameter gt : t -> t -> 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 : t -> t -> 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 t := Z.
Definition zero := 0.
Definition one := 1.
Definition plus := Z.add.
Definition opp := Z.opp.
Definition minus := Z.sub.
Definition mult := Z.mul.
Lemma ring : @ring_theory t zero one plus mult minus opp (@eq t).
Definition le := Z.le.
Definition lt := Z.lt.
Definition ge := Z.ge.
Definition gt := Z.gt.
Definition le_lt_iff := Z.le_ngt.
Definition ge_le_iff := Z.ge_le_iff.
Definition gt_lt_iff := Z.gt_lt_iff.
Definition lt_trans := Z.lt_trans.
Definition lt_not_eq := Z.lt_neq.
Definition lt_0_1 := Z.lt_0_1.
Definition plus_le_compat := Z.add_le_mono.
Definition mult_lt_compat_l := Zmult_lt_compat_l.
Lemma opp_le_compat i j : i<=j -> (-j)<=(-i).
Definition compare := Z.compare.
Definition compare_Eq := Z.compare_eq_iff.
Lemma compare_Lt i j : compare i j = Lt <-> i<j.
Lemma compare_Gt i j : compare i j = Gt <-> i>j.
Definition le_lt_int := Z.lt_le_pred.
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.
Theorem eq_term_refl : forall t0 : term, eq_term t0 t0 = true.
Ltac trivial_case := unfold not; 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); 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); 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); 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; auto; Simplify
| (if bgt ?X1 ?X2 then _ else _) =>
let H := fresh "H" in
elim_bgt X1 X2; intro H; simpl; 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; 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; intros; Simplify; simpl;
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 trace : list t_fusion, term_stable (fusion trace).
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 t_rewrite (s : step) : term -> term :=
match s with
| C_DO_BOTH s1 s2 => apply_both (t_rewrite s1) (t_rewrite s2)
| C_LEFT s => apply_left (t_rewrite s)
| C_RIGHT s => apply_right (t_rewrite s)
| C_SEQ s1 s2 => fun t : term => t_rewrite s2 (t_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 t_rewrite_stable : forall s : step, term_stable (t_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) (t0 i : nat),
valid_hyps (not_exact_divide k1 k2 body t0 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) (t_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 tr : t_omega, valid_list_hyps (execute_omega tr).
Definition move_right (s : step) (p : proposition) :=
match p with
| EqTerm t1 t2 => EqTerm (Tint 0) (t_rewrite s (t1 + - t2)%term)
| LeqTerm t1 t2 => LeqTerm (Tint 0) (t_rewrite s (t2 + - t1)%term)
| GeqTerm t1 t2 => LeqTerm (Tint 0) (t_rewrite s (t1 + - t2)%term)
| LtTerm t1 t2 => LeqTerm (Tint 0) (t_rewrite s (t2 + Tint (-(1)) + - t1)%term)
| GtTerm t1 t2 => LeqTerm (Tint 0) (t_rewrite s (t1 + Tint (-(1)) + - t2)%term)
| NeqTerm t1 t2 => NeqTerm (Tint 0) (t_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 (tr : t_omega) (ep : list Prop) (env : list int) (l : hyps),
interp_list_goal ep env (execute_omega tr 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).