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