diff options
author | 2010-07-21 09:46:51 +0200 | |
---|---|---|
committer | 2010-07-21 09:46:51 +0200 | |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /contrib/micromega/Refl.v | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'contrib/micromega/Refl.v')
-rw-r--r-- | contrib/micromega/Refl.v | 129 |
1 files changed, 0 insertions, 129 deletions
diff --git a/contrib/micromega/Refl.v b/contrib/micromega/Refl.v deleted file mode 100644 index 801d8b21..00000000 --- a/contrib/micromega/Refl.v +++ /dev/null @@ -1,129 +0,0 @@ -(************************************************************************) -(* 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. |