list.why 1.24 KB
Newer Older
1
2
3
4
theory Induction2
  use import list.List
  use import list.Length

Andrei Paskevich's avatar
Andrei Paskevich committed
5
  logic p (list 'a) (list 'b)
6

7
  axiom Induction :
Andrei Paskevich's avatar
Andrei Paskevich committed
8
9
10
11
    p (Nil : list 'a) (Nil : list 'b) ->
    (forall x1:'a, x2:'b, l1:list 'a, l2:list 'b.
       p l1 l2 -> p (Cons x1 l1) (Cons x2 l2)) ->
    forall l1:list 'a, l2:list 'b. length l1 = length l2 -> p l1 l2
12
13
14
15
16
17
18
end

theory Test1
  use export int.Int
  use export list.List
  use export list.Length

Andrei Paskevich's avatar
Andrei Paskevich committed
19
20
  goal G1 : length (Cons 1 Nil) = 1
  goal G2 : length (Cons 1 (Cons 2 Nil)) = 1 + 1
21

Andrei Paskevich's avatar
Andrei Paskevich committed
22
  logic zip (l1 : list 'a) (l2 : list 'b) : list ('a,'b) =
23
    match l1, l2 with
Andrei Paskevich's avatar
Andrei Paskevich committed
24
    | Cons x1 r1, Cons x2 r2 -> Cons (x1,x2) (zip r1 r2)
25
    | _, _ -> Nil (* to make it total *)
26
27
    end

Andrei Paskevich's avatar
Andrei Paskevich committed
28
29
  logic foo (l1 : list 'a) (l2 : list 'b) =
    length (zip l1 l2) = length l1
30
31
32

  clone Induction2 with logic p = foo

Andrei Paskevich's avatar
Andrei Paskevich committed
33
34
35
  lemma G3 : forall l1: list 'a, l2 : list 'b.
    length l1 = length l2 ->
    length (zip l1 l2) = length l1
36

Andrei Paskevich's avatar
Andrei Paskevich committed
37
38
39
  goal G4 : zip (Cons 1  (Cons 2  Nil))
                (Cons 1. (Cons 2. Nil)) =
                Cons (1, 1.) (Cons (2, 2.) Nil)
40

Andrei Paskevich's avatar
Andrei Paskevich committed
41
42
43
44
  goal G5 : forall l1: list 'a, l2 : list 'b, l3: list 'c, l4: list 'd.
    length l1 = length l2 and length l2 = length l3 and
      length l3 = length l4 ->
    length (zip (zip l1 l2) (zip l3 l4)) = length l3
45

46
end