blob: a5d07405e097c646ff40198f32fc830164e1d496 (
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
|
Inductive List [A:Set] :Set :=
Nil:(List A) | Cons:A->(List A)->(List A).
Inductive eqlong : (List nat)-> (List nat)-> Prop :=
eql_cons : (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 : (a:nat)(x:(List nat))
(eqlong (Nil nat) (Cons nat a x))\/ ~(eqlong (Nil nat)(Cons nat a x)).
Parameter V3 : (a:nat)(x:(List nat))
(eqlong (Cons nat a x) (Nil nat))\/ ~(eqlong (Cons nat a x) (Nil nat)).
Parameter V4 : (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 : (n,m:nat)(x,y:(List nat))
~(eqlong x y)-> ~(eqlong (Cons nat n x) (Cons nat m y)).
Parameter inv_r : (n:nat)(x:(List nat)) ~(eqlong (Nil nat) (Cons nat n x)).
Parameter inv_l : (n:nat)(x:(List nat)) ~(eqlong (Cons nat n x) (Nil nat)).
Fixpoint eqlongdec [x:(List nat)]: (y:(List nat))(eqlong x y)\/~(eqlong x y) :=
[y:(List nat)]
<[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases x y of
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) =>
<(eqlong L1 L2) \/~(eqlong L1 L2)>Cases (eqlongdec x y) of
(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
<[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases (Nil nat) (Nil nat) of
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) =>
<(eqlong L1 L2) \/~(eqlong L1 L2)>Cases (eqlongdec x y) of
(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.
|
