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
|
Inductive List (A : Set) : Set :=
| Nil : List A
| Cons : A -> List A -> List A.
Inductive eqlong : List nat -> List nat -> Prop :=
| eql_cons :
forall (n m : nat) (x y : List nat),
eqlong x y -> eqlong (Cons nat n x) (Cons nat m y)
| eql_nil : eqlong (Nil nat) (Nil nat).
Parameter V1 : eqlong (Nil nat) (Nil nat) \/ ~ eqlong (Nil nat) (Nil nat).
Parameter
V2 :
forall (a : nat) (x : List nat),
eqlong (Nil nat) (Cons nat a x) \/ ~ eqlong (Nil nat) (Cons nat a x).
Parameter
V3 :
forall (a : nat) (x : List nat),
eqlong (Cons nat a x) (Nil nat) \/ ~ eqlong (Cons nat a x) (Nil nat).
Parameter
V4 :
forall (a : nat) (x : List nat) (b : nat) (y : List nat),
eqlong (Cons nat a x) (Cons nat b y) \/
~ eqlong (Cons nat a x) (Cons nat b y).
Parameter
nff :
forall (n m : nat) (x y : List nat),
~ eqlong x y -> ~ eqlong (Cons nat n x) (Cons nat m y).
Parameter
inv_r : forall (n : nat) (x : List nat), ~ eqlong (Nil nat) (Cons nat n x).
Parameter
inv_l : forall (n : nat) (x : List nat), ~ eqlong (Cons nat n x) (Nil nat).
Fixpoint eqlongdec (x y : List nat) {struct x} :
eqlong x y \/ ~ eqlong x y :=
match x, y return (eqlong x y \/ ~ eqlong x y) with
| Nil _, Nil _ => or_introl (~ eqlong (Nil nat) (Nil nat)) eql_nil
| Nil _, Cons _ a x as L => or_intror (eqlong (Nil nat) L) (inv_r a x)
| Cons _ a x as L, Nil _ => or_intror (eqlong L (Nil nat)) (inv_l a x)
| Cons _ a x as L1, Cons _ b y as L2 =>
match eqlongdec x y return (eqlong L1 L2 \/ ~ eqlong L1 L2) with
| or_introl h => or_introl (~ eqlong L1 L2) (eql_cons a b x y h)
| or_intror h => or_intror (eqlong L1 L2) (nff a b x y h)
end
end.
Type
match Nil nat as x, Nil nat as y return (eqlong x y \/ ~ eqlong x y) with
| Nil _, Nil _ => or_introl (~ eqlong (Nil nat) (Nil nat)) eql_nil
| Nil _, Cons _ a x as L => or_intror (eqlong (Nil nat) L) (inv_r a x)
| Cons _ a x as L, Nil _ => or_intror (eqlong L (Nil nat)) (inv_l a x)
| Cons _ a x as L1, Cons _ b y as L2 =>
match eqlongdec x y return (eqlong L1 L2 \/ ~ eqlong L1 L2) with
| or_introl h => or_introl (~ eqlong L1 L2) (eql_cons a b x y h)
| or_intror h => or_intror (eqlong L1 L2) (nff a b x y h)
end
end.
|
