summaryrefslogtreecommitdiff
path: root/contrib/dp/test2.v
blob: 3e4c0f6dd0d65a2bea97d92cead887bce9791e04 (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).
Implicit Arguments IN [A].

Goal forall x, forall (l:list nat), IN x l -> IN x (1%nat::l).
  zenon.
Print In.