1
Check (forall A:Type, (exists x:A, forall (y:A), x <> y) -> 2 = 3).
18
Theorem zero_leq_three: 0 <= 3.
31
Lemma zero_leq_three': 0 <= 3.
36
Lemma zero_lt_three : 0 < 3.
43
Inductive le'(n:nat):nat -> Prop :=
45
| le'_S : forall p, le' (S n) p -> le' n p.
47
Hint Constructors le'.
58
Check (nil (A:= nat -> nat)).
60
Check (fun A: Type => (cons (A:=A))).
62
Check (cons 3 (cons 2 nil)).
64
Check (nat :: bool ::nil).
66
Check ((3<=4) :: True ::nil).
68
Check (Prop::Set::nil).
70
Require Import Bvector.
76
Check (fun (A:Type)(a:A)=> Vcons _ a _ (Vnil _)).
78
Check (Vcons _ 5 _ (Vcons _ 3 _ (Vnil _))).
80
Lemma eq_3_3 : 2 + 1 = 3.
86
Lemma eq_proof_proof : refl_equal (2*6) = refl_equal (3*4).
92
Lemma eq_lt_le : ( 2 < 4) = (3 <= 4).
97
Lemma eq_nat_nat : nat = nat.
102
Lemma eq_Set_Set : Set = Set.
107
Lemma eq_Type_Type : Type = Type.
132
Require Import ZArith.
133
Require Import Compare_dec.
137
Definition max (n p :nat) := match le_lt_dec n p with
142
Theorem le_max : forall n p, n <= p -> max n p = p.
144
intros n p ; unfold max ; case (le_lt_dec n p); simpl.
146
intros; absurd (p < p); eauto with arith.
156
Inductive tree(A:Type) : Type :=
157
node : A -> forest A -> tree A
159
forest (A: Type) : Type :=
161
addchild : tree A -> forest A -> forest A.
170
evenS : forall n, odd n -> even (S n)
173
oddS : forall n, even n -> odd (S n).
175
Lemma odd_49 : odd (7 * 7).
176
simpl; repeat constructor.
181
Definition nat_case :=
182
fun (Q : Type)(g0 : Q)(g1 : nat -> Q)(n:nat) =>
183
match n return Q with
188
Eval simpl in (nat_case nat 0 (fun p => p) 34).
190
Eval simpl in (fun g0 g1 => nat_case nat g0 g1 34).
192
Eval simpl in (fun g0 g1 => nat_case nat g0 g1 0).
195
Definition pred (n:nat) := match n with O => O | S m => m end.
197
Eval simpl in pred 56.
199
Eval simpl in pred 0.
201
Eval simpl in fun p => pred (S p).
204
Definition xorb (b1 b2:bool) :=
206
| false, true => true
207
| true, false => true
212
Definition pred_spec (n:nat) := {m:nat | n=0 /\ m=0 \/ n = S m}.
215
Definition predecessor : forall n:nat, pred_spec n.
217
unfold pred_spec;exists 0;auto.
218
unfold pred_spec; intro n0;exists n0; auto.
223
Extraction predecessor.
226
forall n:nat, n = match n with 0 => 0 | S p => S p end.
227
intro n;case n;simpl;auto.
230
Check (fun p:False => match p return 2=3 with end).
232
Theorem fromFalse : False -> 0=1.
237
Section equality_elimination.
242
Check (fun H : Q a =>
243
match p in (eq _ y) return Q y with
247
End equality_elimination.
250
Theorem trans : forall n m p:nat, n=m -> m=p -> n=p.
257
Lemma Rw : forall x y: nat, y = y * x -> y * x * x = y.
258
intros x y e; do 2 rewrite <- e.
263
Require Import Arith.
268
: forall n : nat, 1 * n = n
271
Check mult_plus_distr_r.
274
: forall n m p : nat, (n + m) * p = n * p + m * p
278
Lemma mult_distr_S : forall n p : nat, n * p + p = (S n)* p.
279
simpl;auto with arith.
282
Lemma four_n : forall n:nat, n+n+n+n = 4*n.
283
intro n;rewrite <- (mult_1_l n).
286
intro n; pattern n at 1.
290
repeat rewrite mult_distr_S.
295
Section Le_case_analysis.
296
Variables (n p : nat)
300
(HS : forall m, n <= m -> Q (S m)).
302
match H in (_ <= q) return (Q q) with
304
| le_S m Hm => HS m Hm
309
End Le_case_analysis.
312
Lemma predecessor_of_positive : forall n, 1 <= n -> exists p:nat, n = S p.
316
intros m Hm; exists m;trivial.
319
Definition Vtail_total
320
(A : Type) (n : nat) (v : vector A n) : vector A (pred n):=
321
match v in (vector _ n0) return (vector A (pred n0)) with
323
| Vcons _ n0 v0 => v0
326
Definition Vtail' (A:Type)(n:nat)(v:vector A n) : vector A (pred n).
327
intros A n v; case v.
335
Inductive Lambda : Set :=
336
lambda : (Lambda -> False) -> Lambda.
339
Error: Non strictly positive occurrence of "Lambda" in
340
"(Lambda -> False) -> Lambda"
345
Variable Lambda : Set.
346
Variable lambda : (Lambda -> False) ->Lambda.
348
Variable matchL : Lambda -> forall Q:Prop, ((Lambda ->False) -> Q) -> Q.
350
understand matchL Q l (fun h : Lambda -> False => t)
352
as match l return Q with lambda h => t end
355
Definition application (f x: Lambda) :False :=
356
matchL f False (fun h => h x).
358
Definition Delta : Lambda := lambda (fun x : Lambda => application x x).
360
Definition loop : False := application Delta Delta.
362
Theorem two_is_three : 2 = 3.
370
Require Import ZArith.
374
Inductive itree : Set :=
376
| inode : Z-> (nat -> itree) -> itree.
378
Definition isingle l := inode l (fun i => ileaf).
380
Definition t1 := inode 0 (fun n => isingle (Z_of_nat (2*n))).
382
Definition t2 := inode 0
385
(fun p => isingle (Z_of_nat (n*p)))).
388
Inductive itree_le : itree-> itree -> Prop :=
389
| le_leaf : forall t, itree_le ileaf t
390
| le_node : forall l l' s s',
392
(forall i, exists j:nat, itree_le (s i) (s' j)) ->
393
itree_le (inode l s) (inode l' s').
396
Theorem itree_le_trans :
397
forall t t', itree_le t t' ->
398
forall t'', itree_le t' t'' -> itree_le t t''.
410
inversion_clear H0;eauto with zarith.
412
intro i2; case (H4 i2).
414
generalize (H i2 _ H0).
417
generalize (H5 _ H6).
423
Inductive itree_le' : itree-> itree -> Prop :=
424
| le_leaf' : forall t, itree_le' ileaf t
425
| le_node' : forall l l' s s' g,
427
(forall i, itree_le' (s i) (s' (g i))) ->
428
itree_le' (inode l s) (inode l' s').
434
Lemma t1_le_t2 : itree_le t1 t2.
438
intro i; exists (2 * i).
442
exists i;constructor.
447
Lemma t1_le'_t2 : itree_le' t1 t2.
449
constructor 2 with (fun i : nat => 2 * i).
452
intro i ; constructor 2 with (fun i :nat => i).
460
Inductive ltree (A:Set) : Set :=
461
lnode : A -> list (ltree A) -> ltree A.
463
Inductive prop : Prop :=
464
prop_intro : Prop -> prop.
466
Check (prop_intro prop).
468
Inductive ex_Prop (P : Prop -> Prop) : Prop :=
469
exP_intro : forall X : Prop, P X -> ex_Prop P.
471
Lemma ex_Prop_inhabitant : ex_Prop (fun P => P -> P).
473
exists (ex_Prop (fun P => P -> P)).
482
Check (fun (P:Prop->Prop)(p: ex_Prop P) =>
483
match p with exP_intro X HX => X end).
485
Incorrect elimination of "p" in the inductive type
486
"ex_Prop", the return type has sort "Type" while it should be
489
Elimination of an inductive object of sort "Prop"
490
is not allowed on a predicate in sort "Type"
491
because proofs can be eliminated only to build proofs
496
Inductive typ : Type :=
497
typ_intro : Type -> typ.
499
Definition typ_inject: typ.
505
Error: Universe Inconsistency.
510
Inductive aSet : Set :=
511
aSet_intro: Set -> aSet.
514
User error: Large non-propositional inductive types must be in Type
518
Inductive ex_Set (P : Set -> Prop) : Type :=
519
exS_intro : forall X : Set, P X -> ex_Set P.
522
Inductive comes_from_the_left (P Q:Prop): P \/ Q -> Prop :=
523
c1 : forall p, comes_from_the_left P Q (or_introl (A:=P) Q p).
525
Goal (comes_from_the_left _ _ (or_introl True I)).
529
Goal ~(comes_from_the_left _ _ (or_intror True I)).
535
Reset comes_from_the_left.
544
Definition comes_from_the_left (P Q:Prop)(H:P \/ Q): Prop :=
546
| or_introl p => True
547
| or_intror q => False
551
Incorrect elimination of "H" in the inductive type
552
"or", the return type has sort "Type" while it should be
555
Elimination of an inductive object of sort "Prop"
556
is not allowed on a predicate in sort "Type"
557
because proofs can be eliminated only to build proofs
561
Definition comes_from_the_left_sumbool
562
(P Q:Prop)(x:{P}+{Q}): Prop :=
577
Theorem S_is_not_O : forall n, S n <> 0.
579
Definition Is_zero (x:nat):= match x with
583
Lemma O_is_zero : forall m, m = 0 -> Is_zero m.
587
============================
594
apply O_is_zero with (m := S n).
598
Theorem disc2 : forall n, S (S n) <> 1.
600
intros n Hn; discriminate.
604
Theorem disc3 : forall n, S (S n) = 0 -> forall Q:Prop, Q.
612
Theorem inj_succ : forall n m, S n = S m -> n = m.
616
Lemma inj_pred : forall n m, n = m -> pred n = pred m.
624
apply inj_pred with (n:= S n) (m := S m); assumption.
627
Lemma list_inject : forall (A:Type)(a b :A)(l l':list A),
628
a :: b :: l = b :: a :: l' -> a = b /\ l = l'.
636
Theorem not_le_Sn_0 : forall n:nat, ~ (S n <= 0).
642
Lemma not_le_Sn_0_with_constraints :
643
forall n p , S n <= p -> p = 0 -> False.
645
intros n p H; case H ;
646
intros; discriminate.
649
eapply not_le_Sn_0_with_constraints; eauto.
653
Theorem not_le_Sn_0' : forall n:nat, ~ (S n <= 0).
655
red; intros n H ; inversion H.
658
Derive Inversion le_Sn_0_inv with (forall n :nat, S n <= 0).
661
Theorem le_Sn_0'' : forall n p : nat, ~ S n <= 0 .
664
inversion H using le_Sn_0_inv.
667
Derive Inversion_clear le_Sn_0_inv' with (forall n :nat, S n <= 0).
671
Theorem le_reverse_rules :
672
forall n m:nat, n <= m ->
674
exists p, n <= p /\ m = S p.
676
intros n m H; inversion H.
678
right; exists m0; split; trivial.
680
intros n m H; inversion_clear H.
682
right; exists m0; split; trivial.
685
Inductive ArithExp : Set :=
687
| Succ : ArithExp -> ArithExp
688
| Plus : ArithExp -> ArithExp -> ArithExp.
690
Inductive RewriteRel : ArithExp -> ArithExp -> Prop :=
691
RewSucc : forall e1 e2 :ArithExp,
692
RewriteRel e1 e2 -> RewriteRel (Succ e1) (Succ e2)
693
| RewPlus0 : forall e:ArithExp,
694
RewriteRel (Plus Zero e) e
695
| RewPlusS : forall e1 e2:ArithExp,
697
RewriteRel (Plus (Succ e1) e2) (Succ (Plus e1 e2)).
701
Fixpoint plus (n p:nat) {struct n} : nat :=
704
| S m => S (plus m p)
707
Fixpoint plus' (n p:nat) {struct p} : nat :=
710
| S q => S (plus' n q)
713
Fixpoint plus'' (n p:nat) {struct n} : nat :=
716
| S m => plus'' m (S p)
720
Fixpoint even_test (n:nat) : bool :=
724
| S (S p) => even_test p
730
Fixpoint even_test (n:nat) : bool :=
736
with odd_test (n:nat) : bool :=
745
Eval simpl in even_test.
749
Eval simpl in (fun x : nat => even_test x).
751
Eval simpl in (fun x : nat => plus 5 x).
752
Eval simpl in (fun x : nat => even_test (plus 5 x)).
754
Eval simpl in (fun x : nat => even_test (plus x 5)).
757
Section Principle_of_Induction.
758
Variable P : nat -> Prop.
759
Hypothesis base_case : P 0.
760
Hypothesis inductive_step : forall n:nat, P n -> P (S n).
761
Fixpoint nat_ind (n:nat) : (P n) :=
762
match n return P n with
764
| S m => inductive_step m (nat_ind m)
767
End Principle_of_Induction.
769
Scheme Even_induction := Minimality for even Sort Prop
770
with Odd_induction := Minimality for odd Sort Prop.
772
Theorem even_plus_four : forall n:nat, even n -> even (4+n).
775
elim H using Even_induction with (P0 := fun n => odd (4+n));
776
simpl;repeat constructor;assumption.
780
Section Principle_of_Double_Induction.
781
Variable P : nat -> nat ->Prop.
782
Hypothesis base_case1 : forall x:nat, P 0 x.
783
Hypothesis base_case2 : forall x:nat, P (S x) 0.
784
Hypothesis inductive_step : forall n m:nat, P n m -> P (S n) (S m).
785
Fixpoint nat_double_ind (n m:nat){struct n} : P n m :=
786
match n, m return P n m with
787
| 0 , x => base_case1 x
788
| (S x), 0 => base_case2 x
789
| (S x), (S y) => inductive_step x y (nat_double_ind x y)
791
End Principle_of_Double_Induction.
793
Section Principle_of_Double_Recursion.
794
Variable P : nat -> nat -> Type.
795
Hypothesis base_case1 : forall x:nat, P 0 x.
796
Hypothesis base_case2 : forall x:nat, P (S x) 0.
797
Hypothesis inductive_step : forall n m:nat, P n m -> P (S n) (S m).
798
Fixpoint nat_double_rect (n m:nat){struct n} : P n m :=
799
match n, m return P n m with
800
| 0 , x => base_case1 x
801
| (S x), 0 => base_case2 x
802
| (S x), (S y) => inductive_step x y (nat_double_rect x y)
804
End Principle_of_Double_Recursion.
806
Definition min : nat -> nat -> nat :=
807
nat_double_rect (fun (x y:nat) => nat)
810
(fun (x y r:nat) => S r).
812
Eval compute in (min 5 8).
813
Eval compute in (min 8 5).
817
Lemma not_circular : forall n:nat, n <> S n.
820
apply nat_ind with (P:= fun n => n <> S n).
822
red; intros n0 Hn0 eqn0Sn0;injection eqn0Sn0;trivial.
825
Definition eq_nat_dec : forall n p:nat , {n=p}+{n <> p}.
828
apply nat_double_rect with (P:= fun (n q:nat) => {q=p}+{q <> p}).
831
elim n using nat_double_rect.
834
intros n0 m H; case H.
835
intro eq; rewrite eq ; auto.
836
intro neg; right; red ; injection 1; auto.
839
Definition eq_nat_dec' : forall n p:nat, {n=p}+{n <> p}.
846
Lemma le'_le : forall n p, le' n p -> n <= p.
848
induction 1;auto with arith.
851
Lemma le'_n_Sp : forall n p, le' n p -> le' n (S p).
856
Hint Resolve le'_n_Sp.
859
Lemma le_le' : forall n p, n<=p -> le' n p.
861
induction 1;auto with arith.
868
Require Import Minus.
871
Fixpoint div (x y:nat){struct x}: nat :=
874
else if eq_nat_dec y 0
876
else S (div (x-y) y).
879
Recursive definition of div is ill-formed.
881
div : nat -> nat -> nat
887
Recursive call to div has principal argument equal to
889
instead of a subterm of x
893
Lemma minus_smaller_S: forall x y:nat, x - y < S x.
895
intros x y; pattern y, x;
896
elim x using nat_double_ind.
897
destruct x0; auto with arith.
898
simpl; auto with arith.
899
simpl; auto with arith.
902
Lemma minus_smaller_positive : forall x y:nat, x <>0 -> y <> 0 ->
905
destruct x; destruct y;
906
( simpl;intros; apply minus_smaller_S ||
907
intros; absurd (0=0); auto).
910
Definition minus_decrease : forall x y:nat, Acc lt x ->
915
intros x y H; case H.
917
apply Hz; apply minus_smaller_positive; assumption.
920
Print minus_decrease.
924
Definition div_aux (x y:nat)(H: Acc lt x):nat.
927
refine (if eq_nat_dec x 0
929
else if eq_nat_dec y 0
931
else div_aux (x-y) y _).
932
apply (minus_decrease x y H);assumption.
939
(fix div_aux (x y : nat) (H : Acc lt x) {struct H} : nat :=
940
match eq_nat_dec x 0 with
943
match eq_nat_dec y 0 with
945
| right _0 => div_aux (x - y) y (minus_decrease x y H _ _0)
948
: forall x : nat, nat -> Acc lt x -> nat
951
Require Import Wf_nat.
952
Definition div x y := div_aux x y (lt_wf x).
963
let rec div_aux x y =
964
match eq_nat_dec x O with
967
(match eq_nat_dec y O with
969
| Right -> div_aux (minus x y) y)
972
Lemma vector0_is_vnil : forall (A:Type)(v:vector A 0), v = Vnil A.
974
intros A v;inversion v.
978
Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:vector A n),
981
Toplevel input, characters 40281-40287
982
> Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n), n= 0 -> v = Vnil A.
984
Error: In environment
989
The term "Vnil A" has type "vector A 0" while it is expected to have type
995
(* On devrait changer Set en Type ? *)
997
Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:vector A n),
998
n= 0 -> JMeq v (Vnil A).
1002
intro; discriminate.
1005
Lemma vector0_is_vnil : forall (A:Type)(v:vector A 0), v = Vnil A.
1007
intros a v;apply JMeq_eq.
1008
apply vector0_is_vnil_aux.
1013
Implicit Arguments Vcons [A n].
1014
Implicit Arguments Vnil [A].
1015
Implicit Arguments Vhead [A n].
1016
Implicit Arguments Vtail [A n].
1018
Definition Vid : forall (A : Type)(n:nat), vector A n -> vector A n.
1020
destruct n; intro v.
1022
exact (Vcons (Vhead v) (Vtail v)).
1025
Eval simpl in (fun (A:Type)(v:vector A 0) => (Vid _ _ v)).
1027
Eval simpl in (fun (A:Type)(v:vector A 0) => v).
1031
Lemma Vid_eq : forall (n:nat) (A:Type)(v:vector A n), v=(Vid _ n v).
1038
Theorem zero_nil : forall A (v:vector A 0), v = Vnil.
1041
change (Vnil (A:=A)) with (Vid _ 0 v).
1047
forall (A : Type) (n : nat) (v : vector A (S n)),
1048
v = Vcons (Vhead v) (Vtail v).
1051
change (Vcons (Vhead v) (Vtail v)) with (Vid _ (S n) v).
1057
Definition vector_double_rect :
1058
forall (A:Type) (P: forall (n:nat),(vector A n)->(vector A n) -> Type),
1060
(forall n (v1 v2 : vector A n) a b, P n v1 v2 ->
1061
P (S n) (Vcons a v1) (Vcons b v2)) ->
1062
forall n (v1 v2 : vector A n), P n v1 v2.
1064
intros; rewrite (zero_nil _ v1); rewrite (zero_nil _ v2).
1066
intros v1 v2; rewrite (decomp _ _ v1);rewrite (decomp _ _ v2).
1070
Require Import Bool.
1072
Definition bitwise_or n v1 v2 : vector bool n :=
1073
vector_double_rect bool (fun n v1 v2 => vector bool n)
1075
(fun n v1 v2 a b r => Vcons (orb a b) r) n v1 v2.
1078
Fixpoint vector_nth (A:Type)(n:nat)(p:nat)(v:vector A p){struct v}
1082
| 0 , Vcons b _ _ => Some b
1083
| S n', Vcons _ p' v' => vector_nth A n' p' v'
1086
Implicit Arguments vector_nth [A p].
1089
Lemma nth_bitwise : forall (n:nat) (v1 v2: vector bool n) i a b,
1090
vector_nth i v1 = Some a ->
1091
vector_nth i v2 = Some b ->
1092
vector_nth i (bitwise_or _ v1 v2) = Some (orb a b).
1094
intros n v1 v2; pattern n,v1,v2.
1095
apply vector_double_rect.
1097
destruct i; discriminate 1.
1098
destruct i; simpl;auto.
1099
injection 1; injection 2;intros; subst a; subst b; auto.
1102
Set Implicit Arguments.
1104
CoInductive Stream (A:Type) : Type :=
1105
| Cons : A -> Stream A -> Stream A.
1107
CoInductive LList (A: Type) : Type :=
1109
| LCons : A -> LList A -> LList A.
1115
Definition head (A:Type)(s : Stream A) := match s with Cons a s' => a end.
1117
Definition tail (A : Type)(s : Stream A) :=
1118
match s with Cons a s' => s' end.
1120
CoFixpoint repeat (A:Type)(a:A) : Stream A := Cons a (repeat a).
1122
CoFixpoint iterate (A: Type)(f: A -> A)(a : A) : Stream A:=
1123
Cons a (iterate f (f a)).
1125
CoFixpoint map (A B:Type)(f: A -> B)(s : Stream A) : Stream B:=
1126
match s with Cons a tl => Cons (f a) (map f tl) end.
1128
Eval simpl in (fun (A:Type)(a:A) => repeat a).
1130
Eval simpl in (fun (A:Type)(a:A) => head (repeat a)).
1133
CoInductive EqSt (A: Type) : Stream A -> Stream A -> Prop :=
1134
eqst : forall s1 s2: Stream A,
1135
head s1 = head s2 ->
1136
EqSt (tail s1) (tail s2) ->
1140
Section Parks_Principle.
1142
Variable R : Stream A -> Stream A -> Prop.
1143
Hypothesis bisim1 : forall s1 s2:Stream A, R s1 s2 ->
1145
Hypothesis bisim2 : forall s1 s2:Stream A, R s1 s2 ->
1146
R (tail s1) (tail s2).
1148
CoFixpoint park_ppl : forall s1 s2:Stream A, R s1 s2 ->
1150
fun s1 s2 (p : R s1 s2) =>
1151
eqst s1 s2 (bisim1 p)
1152
(park_ppl (bisim2 p)).
1153
End Parks_Principle.
1156
Theorem map_iterate : forall (A:Type)(f:A->A)(x:A),
1157
EqSt (iterate f (f x)) (map f (iterate f x)).
1161
(R:= fun s1 s2 => exists x: A,
1162
s1 = iterate f (f x) /\ s2 = map f (iterate f x)).
1164
intros s1 s2 (x0,(eqs1,eqs2));rewrite eqs1;rewrite eqs2;reflexivity.
1165
intros s1 s2 (x0,(eqs1,eqs2)).
1166
exists (f x0);split;[rewrite eqs1|rewrite eqs2]; reflexivity.
1167
exists x;split; reflexivity.
1170
Ltac infiniteproof f :=
1171
cofix f; constructor; [clear f| simpl; try (apply f; clear f)].
1174
Theorem map_iterate' : forall (A:Type)(f:A->A)(x:A),
1175
EqSt (iterate f (f x)) (map f (iterate f x)).
1176
infiniteproof map_iterate'.
1181
Implicit Arguments LNil [A].
1183
Lemma Lnil_not_Lcons : forall (A:Type)(a:A)(l:LList A),
1184
LNil <> (LCons a l).
1185
intros;discriminate.
1188
Lemma injection_demo : forall (A:Type)(a b : A)(l l': LList A),
1189
LCons a (LCons b l) = LCons b (LCons a l') ->
1192
intros A a b l l' e; injection e; auto.
1196
Inductive Finite (A:Type) : LList A -> Prop :=
1197
| Lnil_fin : Finite (LNil (A:=A))
1198
| Lcons_fin : forall a l, Finite l -> Finite (LCons a l).
1200
CoInductive Infinite (A:Type) : LList A -> Prop :=
1201
| LCons_inf : forall a l, Infinite l -> Infinite (LCons a l).
1203
Lemma LNil_not_Infinite : forall (A:Type), ~ Infinite (LNil (A:=A)).
1205
intros A H;inversion H.
1208
Lemma Finite_not_Infinite : forall (A:Type)(l:LList A),
1209
Finite l -> ~ Infinite l.
1211
intros A l H; elim H.
1212
apply LNil_not_Infinite.
1213
intros a l0 F0 I0' I1.
1214
case I0'; inversion_clear I1.
1218
Lemma Not_Finite_Infinite : forall (A:Type)(l:LList A),
1219
~ Finite l -> Infinite l.
1223
intro; absurd (Finite (LNil (A:=A)));[auto|constructor].
1226
red; intro H1;case H0.
added
removed
RecTutorial/RecTutorial.v
