blob: ce660052078261c6002a05423d5f7a7777e5f070 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
Require Import ZArith.
Require Import Classical.
Require Import List.
Open Scope list_scope.
Open Scope Z_scope.
Dp_debug.
Dp_timeout 3.
Require Export zenon.
Definition neg (z:Z) : Z := match z with
| Z0 => Z0
| Zpos p => Zneg p
| Zneg p => Zpos p
end.
Goal forall z, neg (neg z) = z.
Admitted.
Open Scope nat_scope.
Print plus.
Goal forall x, x+0=x.
induction x; ergo.
(* simplify resoud le premier, pas le second *)
Admitted.
Goal 1::2::3::nil = 1::2::(1+2)::nil.
zenon.
Admitted.
Definition T := nat.
Parameter fct : T -> nat.
Goal fct O = O.
Admitted.
Fixpoint even (n:nat) : Prop :=
match n with
O => True
| S O => False
| S (S p) => even p
end.
Goal even 4%nat.
try zenon.
Admitted.
Definition p (A B:Set) (a:A) (b:B) : list (A*B) := cons (a,b) nil.
Definition head :=
fun (A : Set) (l : list A) =>
match l with
| nil => None (A:=A)
| x :: _ => Some x
end.
Goal forall x, head _ (p _ _ 1 2) = Some x -> fst x = 1.
Admitted.
(*
BUG avec head prédéfini : manque eta-expansion sur A:Set
Goal forall x, head _ (p _ _ 1 2) = Some x -> fst x = 1.
Print value.
Print Some.
zenon.
*)
Inductive IN (A:Set) : A -> list A -> Prop :=
| IN1 : forall x l, IN A x (x::l)
| IN2: forall x l, IN A x l -> forall y, IN A x (y::l).
Arguments IN [A] _ _.
Goal forall x, forall (l:list nat), IN x l -> IN x (1%nat::l).
zenon.
Print In.
|
