← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to contrib/micromega/Refl.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

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