← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test-suite/bugs/closed/shouldsucceed/846.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:
test-suite/bugs/closed/shouldsucceed/846.v
 
1
Set Implicit Arguments.
 
2
 
 
3
Open Scope type_scope.
 
4
 
 
5
Inductive One : Set := inOne: One.
 
6
 
 
7
Definition maybe: forall A B:Set,(A -> B) -> One + A -> One + B.
 
8
Proof.
 
9
  intros A B f c.
 
10
  case c.
 
11
  left; assumption.
 
12
  right; apply f; assumption.
 
13
Defined.
 
14
 
 
15
Definition id (A:Set)(a:A):=a.
 
16
 
 
17
Definition LamF (X: Set -> Set)(A:Set) :Set :=
 
18
  A + (X A)*(X A) + X(One + A).
 
19
 
 
20
Definition LamF' (X: Set -> Set)(A:Set) :Set :=
 
21
  LamF X A.
 
22
 
 
23
Require Import List.
 
24
Require Import Bool.
 
25
 
 
26
Definition index := list bool.
 
27
 
 
28
Inductive L (A:Set) : index -> Set :=
 
29
  initL: A -> L A nil
 
30
  | pluslL: forall l:index, One -> L A (false::l) 
 
31
  | plusrL: forall l:index, L A l -> L A (false::l)
 
32
  | varL: forall l:index, L A l -> L A (true::l)
 
33
  | appL: forall l:index, L A (true::l) -> L A (true::l) -> L A (true::l)
 
34
  | absL: forall l:index, L A (true::false::l) -> L A (true::l).
 
35
 
 
36
Scheme L_rec_simp := Minimality for L Sort Set.
 
37
 
 
38
Definition Lam' (A:Set) := L A (true::nil).
 
39
 
 
40
Definition aczelapp: forall (l1 l2: index)(A:Set), L (L A l2) l1 -> L A
 
41
  (l1++l2).
 
42
Proof.
 
43
  intros l1 l2 A.
 
44
  generalize l1.
 
45
  clear l1.
 
46
  (* Check (fun i:index => L A (i++l2)). *)
 
47
  apply (L_rec_simp (A:=L A l2) (fun i:index => L A (i++l2))).
 
48
  trivial.
 
49
  intros l o.
 
50
  simpl app.
 
51
  apply pluslL; assumption.
 
52
  intros l _ t.
 
53
  simpl app.
 
54
  apply plusrL; assumption.
 
55
  intros l _ t.
 
56
  simpl app.
 
57
  apply varL; assumption.
 
58
  intros l _ t1 _ t2.
 
59
  simpl app in *|-*.
 
60
  Check 0.
 
61
  apply appL; [exact t1| exact t2].
 
62
  intros l _ t.
 
63
  simpl app in *|-*.
 
64
  Check 0.
 
65
  apply absL; assumption.
 
66
Defined.
 
67
 
 
68
Definition monL: forall (l:index)(A:Set)(B:Set), (A->B) -> L A l -> L B l.
 
69
Proof.
 
70
  intros l A B f.
 
71
  intro t.
 
72
  elim t.
 
73
  intro a.
 
74
  exact (initL (f a)).
 
75
  intros i u.
 
76
  exact (pluslL _ _ u).
 
77
  intros i _ r.
 
78
  exact (plusrL r).
 
79
  intros i _ r.
 
80
  exact (varL r).
 
81
  intros i _ r1 _ r2.
 
82
  exact (appL r1 r2).
 
83
  intros i _ r.
 
84
  exact (absL r).
 
85
Defined.
 
86
 
 
87
Definition lam': forall (A B:Set), (A -> B) -> Lam' A -> Lam' B.
 
88
Proof.
 
89
  intros A B f t.
 
90
  unfold Lam' in *|-*.
 
91
  Check 0.
 
92
  exact (monL f t).
 
93
Defined.
 
94
 
 
95
Definition inLam': forall A:Set, LamF' Lam' A -> Lam' A.
 
96
Proof.
 
97
  intros A [[a|[t1 t2]]|r].
 
98
  unfold Lam'.
 
99
  exact (varL (initL a)).
 
100
  exact (appL t1 t2).
 
101
  unfold Lam' in * |- *.
 
102
  Check 0.
 
103
  apply absL.
 
104
  change (L A ((true::nil) ++ (false::nil))).
 
105
  apply aczelapp.
 
106
  (* Check (fun x:One + A =>  (match (maybe (fun a:A => initL a) x) with
 
107
    | inl u => pluslL _ _ u
 
108
    | inr t' => plusrL t' end)). *)
 
109
  exact (monL (fun x:One + A =>
 
110
    (match (maybe (fun a:A => initL a) x) with
 
111
       | inl u => pluslL _ _ u
 
112
       | inr t' => plusrL t' end)) r). 
 
113
Defined.
 
114
 
 
115
Section minimal.
 
116
 
 
117
Definition sub1 (F G: Set -> Set):= forall A:Set, F A->G A.
 
118
Hypothesis G: Set -> Set.
 
119
Hypothesis step: sub1 (LamF' G) G.
 
120
 
 
121
Fixpoint L'(A:Set)(i:index){struct i} : Set :=
 
122
  match i with 
 
123
    nil => A
 
124
    | false::l => One + L' A l
 
125
    | true::l => G (L' A l)
 
126
  end. 
 
127
 
 
128
Definition LinL': forall (A:Set)(i:index), L A i -> L' A i.
 
129
Proof.
 
130
  intros A i t.
 
131
  elim t.
 
132
  intro a.
 
133
  unfold L'.
 
134
  assumption.
 
135
  intros l u.
 
136
  left; assumption.
 
137
  intros l _ r.
 
138
  right; assumption.
 
139
  intros l _ r.
 
140
  apply (step (A:=L' A l)).
 
141
  exact (inl _ (inl _ r)).
 
142
  intros l _ r1 _ r2.
 
143
  apply (step (A:=L' A l)).
 
144
  (* unfold L' in * |- *.
 
145
  Check 0. *)
 
146
  exact (inl _ (inr _ (pair r1 r2))).
 
147
  intros l _ r.
 
148
  apply  (step (A:=L' A l)).
 
149
  exact (inr _ r).
 
150
Defined.
 
151
 
 
152
Definition L'inG: forall A: Set, L' A (true::nil) -> G A.
 
153
Proof.
 
154
  intros A t.
 
155
  unfold L' in t.
 
156
  assumption.
 
157
Defined.
 
158
 
 
159
Definition Itbasic: sub1 Lam' G.
 
160
Proof.
 
161
  intros A t.
 
162
  apply L'inG.
 
163
  unfold Lam' in t.
 
164
  exact (LinL' t).
 
165
Defined.
 
166
 
 
167
End minimal.
 
168
 
 
169
Definition recid := Itbasic inLam'.
 
170
 
 
171
Definition L'Lam'inL: forall (i:index)(A:Set), L' Lam' A i -> L A i.
 
172
Proof.
 
173
  intros i A t.
 
174
  induction i.
 
175
  unfold L' in t.
 
176
  apply initL.
 
177
  assumption.
 
178
  induction a.
 
179
  simpl L' in t.
 
180
  apply (aczelapp (l1:=true::nil) (l2:=i)). 
 
181
  exact (lam' IHi t).
 
182
  simpl L' in t.
 
183
  induction t.
 
184
  exact (pluslL _ _ a).
 
185
  exact (plusrL (IHi b)).
 
186
Defined.
 
187
 
 
188
 
 
189
Lemma recidgen: forall(A:Set)(i:index)(t:L A i), L'Lam'inL i A (LinL' inLam' t)
 
190
  = t.
 
191
Proof.
 
192
  intros A i t.
 
193
  induction t.
 
194
  trivial.
 
195
  trivial.
 
196
  simpl.
 
197
  rewrite IHt.
 
198
  trivial.
 
199
  simpl L'Lam'inL.
 
200
  rewrite IHt.
 
201
  trivial.
 
202
  simpl L'Lam'inL.
 
203
  simpl L'Lam'inL in IHt1.
 
204
  unfold lam' in IHt1.
 
205
  simpl L'Lam'inL in IHt2.
 
206
  unfold lam' in IHt2.
 
207
 
 
208
  (* going on. This fails for the original solution. *)
 
209
  rewrite IHt1.
 
210
  rewrite IHt2.
 
211
  trivial.
 
212
Abort. (* one goal still left *)
 
213