proofs/signatures/example-arrays.plf

   1 ; to check, run : lfsc sat.plf smt.plf th_base.plf example.plf
   2
   3 ; --------------------------------------------------------------------------------
   4 ; literals :
   5 ; L1 : a = write( a, i, read( a, i )
   6 ; L2 : read( a, k ) = read( write( a, i, read( a, i ) ), k )
   7 ; L3 : i = k
   8
   9 ; input :
  10 ; ~L1
  11
  12 ; (extenstionality) lemma :
  13 ; L1 or ~L2
  14
  15 ; theory conflicts :
  16 ; L2 or ~L3
  17 ; L2 or L3
  18
  19
  20 ;  With the theory lemma, the input is unsatisfiable.
  21 ; --------------------------------------------------------------------------------
  22
  23
  24 ; (0) -------------------- term declarations -----------------------------------
  25
  26 (check
  27 (% I sort
  28 (% E sort
  29 (% a (term (Array I E))
  30 (% i (term I)
  31
  32
  33 ; (1) -------------------- input formula -----------------------------------
  34
  35 (% A1 (th_holds (not (= (Array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i)))))
  36
  37
  38
  39
  40 ; (2) ------------------- specify that the following is a proof of the empty clause -----------------
  41
  42 (: (holds cln)
  43
  44
  45
  46
  47 ; (3) -------------------- theory lemmas prior to rewriting/preprocess/CNF -----------------
  48 ;     ---  these should introduce (th_holds ...)
  49
  50
  51 ; extensionality lemma : notice this also introduces skolem k
  52 (ext _ _ a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i)) (\ k (\ A2
  53
  54
  55
  56
  57 ; (4) -------------------- map theory literals to boolean variables
  58 ;     --- maps all theory literals involved in proof to boolean literals
  59
  60 (decl_atom (= (Array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) (\ v1 (\ a1
  61 (decl_atom (= E (apply _ _ (apply _ _ (read I E) a) k) (apply _ _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) k)) (\ v2 (\ a2
  62 (decl_atom (= I i k) (\ v3 (\ a3
  63
  64
  65
  66 ; (5) -------------------- theory conflicts ---------------------------------------------
  67 ;     ---  these should introduce (holds ...)
  68
  69 (satlem _ _
  70 (asf _ _ _ a3 (\ l3
  71 (asf _ _ _ a2 (\ l2
  72 (clausify_false
  73
  74    ; use read over write rule "row"
  75    (contra _ (symm _ _ _ (row _ _ _ _ a (apply _ _ (apply _ _ (read I E) a) i) l3)) l2)
  76
  77 ))))) (\ CT1
  78 ; CT1 is the clause ( v2 V v3 )
  79
  80 (satlem _ _
  81 (ast _ _ _ a3 (\ l3
  82 (asf _ _ _ a2 (\ l2
  83 (clausify_false
  84
  85    ; use read over write rule "row1"
  86    (contra _ (symm _ _ _
  87              (trans _ _ _ _
  88                (symm _ _ _ (cong _ _ _ _ _ _
  89                  (refl _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))))
  90                  l3))
  91                (trans _ _ _ _
  92                  (row1 _ _ a i (apply _ _ (apply _ _ (read I E) a) i))
  93                  (cong _ _ _ _ _ _ (refl _ (apply _ _ (read I E) a)) l3)
  94                  )))
  95             l2)
  96
  97 ))))) (\ CT2
  98 ; CT2 is the clause ( v2 V ~v3 )
  99
 100
 101 ; (6) -------------------- clausification -----------------------------------------
 102 ;     ---  these should introduce (holds ...)
 103
 104 (satlem _ _
 105 (ast _ _ _ a1 (\ l1
 106 (clausify_false
 107
 108 ; input formula A1 is ( ~a1 )
 109 ; the following is a proof of a1 ^ ( ~a1 ) => false
 110
 111   (contra _ l1 A1)
 112
 113 ))) (\ C1
 114 ; C1 is the clause ( ~v1 )
 115
 116
 117 (satlem _ _
 118 (asf _ _ _ a1 (\ l1
 119 (ast _ _ _ a2 (\ l2
 120 (clausify_false
 121
 122 ; lemma A2 is ( a1 V ~a2 )
 123 ; the following is a proof of ~a1 ^ a2 ^ ( a1 V ~a2 ) => false
 124
 125   (contra _ l2 (or_elim_1 _ _ l1 A2))
 126
 127 ))))) (\ C2
 128 ; C2 is the clause ( v1 V ~v2 )
 129
 130
 131 ; (7) -------------------- resolution proof ------------------------------------------------------------
 132
 133 (satlem_simplify _ _ _
 134
 135 (R _ _ (R _ _ CT1 CT2 v3) (R _ _ C2 C1 v1) v2)
 136
 137 (\ x x))
 138
 139 )))))))))))))))))))))))))))