Library Coq.micromega.Refl
Require Import List.
Require Setoid.
Set Implicit Arguments.
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.
Theorem make_impl_map :
forall (
A B:
Type) (
eval :
A -> Prop) (
eval' :
A*B -> Prop) (
l :
list (
A*B))
r
(
EVAL :
forall x,
eval' x <-> eval (
fst x)),
make_impl eval' l r <-> make_impl eval (
List.map fst l)
r.
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.
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.
Lemma make_conj_in :
forall (
A :
Type) (
eval :
A -> Prop) (
l :
list A),
make_conj eval l -> (forall p,
In p l -> eval p).
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.
Infix "+++" :=
rev_append (
right associativity,
at level 60) :
list_scope.
Lemma make_conj_rapp :
forall A eval l1 l2, @
make_conj A eval (
l1 +++ l2)
<-> @
make_conj A eval (
l1++l2).
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).
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).