blob: 801d8b2122124cdc1bc97666e1026ddd0cea3af2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* *)
(* Micromega: A reflexive tactic using the Positivstellensatz *)
(* *)
(* Frédéric Besson (Irisa/Inria) 2006-2008 *)
(* *)
(************************************************************************)
Require Import List.
Require Setoid.
Set Implicit Arguments.
(* Refl of '->' '/\': basic properties *)
Fixpoint make_impl (A : Type) (eval : A -> Prop) (l : list A) (goal : Prop) {struct l} : Prop :=
match l with
| nil => goal
| cons e l => (eval e) -> (make_impl eval l goal)
end.
Theorem make_impl_true :
forall (A : Type) (eval : A -> Prop) (l : list A), make_impl eval l True.
Proof.
induction l as [| a l IH]; simpl.
trivial.
intro; apply IH.
Qed.
Fixpoint make_conj (A : Type) (eval : A -> Prop) (l : list A) {struct l} : Prop :=
match l with
| nil => True
| cons e nil => (eval e)
| cons e l2 => ((eval e) /\ (make_conj eval l2))
end.
Theorem make_conj_cons : forall (A : Type) (eval : A -> Prop) (a : A) (l : list A),
make_conj eval (a :: l) <-> eval a /\ make_conj eval l.
Proof.
intros; destruct l; simpl; tauto.
Qed.
Lemma make_conj_impl : forall (A : Type) (eval : A -> Prop) (l : list A) (g : Prop),
(make_conj eval l -> g) <-> make_impl eval l g.
Proof.
induction l.
simpl.
tauto.
simpl.
intros.
destruct l.
simpl.
tauto.
generalize (IHl g).
tauto.
Qed.
Lemma make_conj_in : forall (A : Type) (eval : A -> Prop) (l : list A),
make_conj eval l -> (forall p, In p l -> eval p).
Proof.
induction l.
simpl.
tauto.
simpl.
intros.
destruct l.
simpl in H0.
destruct H0.
subst; auto.
tauto.
destruct H.
destruct H0.
subst;auto.
apply IHl; auto.
Qed.
Lemma make_conj_app : forall A eval l1 l2, @make_conj A eval (l1 ++ l2) <-> @make_conj A eval l1 /\ @make_conj A eval l2.
Proof.
induction l1.
simpl.
tauto.
intros.
change ((a::l1) ++ l2) with (a :: (l1 ++ l2)).
rewrite make_conj_cons.
rewrite IHl1.
rewrite make_conj_cons.
tauto.
Qed.
Lemma not_make_conj_cons : forall (A:Type) (t:A) a eval (no_middle_eval : (eval t) \/ ~ (eval t)),
~ make_conj eval (t ::a) -> ~ (eval t) \/ (~ make_conj eval a).
Proof.
intros.
simpl in H.
destruct a.
tauto.
tauto.
Qed.
Lemma not_make_conj_app : forall (A:Type) (t:list A) a eval
(no_middle_eval : forall d, eval d \/ ~ eval d) ,
~ make_conj eval (t ++ a) -> (~ make_conj eval t) \/ (~ make_conj eval a).
Proof.
induction t.
simpl.
tauto.
intros.
simpl ((a::t)++a0)in H.
destruct (@not_make_conj_cons _ _ _ _ (no_middle_eval a) H).
left ; red ; intros.
apply H0.
rewrite make_conj_cons in H1.
tauto.
destruct (IHt _ _ no_middle_eval H0).
left ; red ; intros.
apply H1.
rewrite make_conj_cons in H2.
tauto.
right ; auto.
Qed.
|
