CCGRID26_code/list.ath at main · FLAGlab/CCGRID26_code · GitHub

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
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109

datatype (Lst S) := empty | (lst head:S tail:(Lst S))

module Lst {

  assert lst-dt-axioms := (datatype-axioms "Lst")
  assert lst-se-axioms := (selector-axioms "Lst")

  define [lst-no-conf-empty lst-no-conf-lst lst-no-junk] := lst-dt-axioms
  define [lst-head lst-tail] := lst-se-axioms

  declare isEmpty: (S) [(Lst S)] -> Boolean

  # assert isEmpty-axioms:=
  #   (fun
  #    [(isEmpty l) =
  #                   [true  when (l = empty)
  # 		   false when (~ l = empty)]])

  # define [isEmpty-true-axiom isEmpty-false-axiom] := isEmpty-axioms

  define [l] := [?l:(Lst 'S)]

  assert* isEmpty-axiom := ((isEmpty l) <==> (l = empty))

  define isEmpty-emptyList := (isEmpty empty)

  conclude isEmpty-emptyList
    (!chain<- [    (isEmpty empty)
        <== (empty = empty) [isEmpty-axiom]])

  define [h t] := [?h:'S ?t:(Lst 'S)]

  define isEmpty-nonEmptyList :=
    (forall h t . (~ isEmpty (lst h t)))

  conclude isEmpty-nonEmptyList
    pick-any h t
    (!chain-> [    true
        ==> (~ (empty = (lst h t)))         [lst-no-conf-empty]
        ==> (~ ((lst h t) = empty))         [sym]
        ==> (~ isEmpty (lst h t))           [isEmpty-axiom]])

  # conclude isEmpty-nonEmptyList
  #   pick-any h t
  #     (!mp (!uspec isEmpty-false-axiom (lst h t))
  # 	 (!sym (!instance lst-no-conf-empty [h t])))


  #define isEmpty->empty :=
  #  (forall l . isEmpty l ==> l = empty)
  #
  # conclude isEmpty->empty
  #   pick-any l
  #     (!chain-> [(isEmpty l) ==> (l = empty) [isEmpty-axiom]])

  assert empty-head := (forall h . ~ ((head empty) = h))
  assert empty-tail := (forall t . ~ ((tail empty) = t))

  define empty-nohead :=
    (forall l . l = empty ==> forall h . (~ head l = h))

  #cvarela: Exercise solution:
  conclude empty-nohead
    pick-any l
      assume (l = empty)
        pick-any h
          let {-head-empty-h := (!uspec empty-head h)}
          (!chain<- [    (~ head l = h)
        <== -head-empty-h  [(l = empty)]])

  define empty-notail :=
    (forall l . l = empty ==> forall t . (~ tail l = t))

  #cvarela: Exercise solution:
  conclude empty-notail
    pick-any l
      assume (l = empty)
        pick-any t
          let {-tail-empty-t := (!uspec empty-tail t)}
          (!chain<- [    (~ tail l = t)
        <== -tail-empty-t  [(l = empty)]])

  define hasHead->notEmpty :=
    (forall l . (exists h . head l = h) ==> ~ isEmpty l)

  #cvarela: Exercise solution:
  conclude hasHead->notEmpty
  pick-any l
    assume e := (exists h . head l = h)
      (!by-contradiction (~ isEmpty l)
        assume (isEmpty l)
    let {_ := (!chain-> [(isEmpty l) ==> (l = empty) [isEmpty-axiom]])}
          (!absurd (!qn (!fire empty-nohead [l])) e))

  define [v h t] := [?v:'S ?h:'S ?t:(Lst 'S)]

  declare in: (S) [S (Lst S)] -> Boolean
  assert in_axioms := ( fun [
    (in v empty) = false
    (in v (lst h t)) = [
      true when (v = h)
      (in v t) when (~ v = h)
    ]
  ])

} # close module Lst

open Lst