(load-file "elms-defs.ath") ; The following method takes two sets s1, s2 such that ;; (s1 subset s2) and an element x in s1 and proves x in s2: (primitive-method (pf P props) (match (prove-from P props) (true P) (_ (print ("\nOtter failed."))))) (define (t p) (print (head (make-otter-prop-string [p])))) (define (subset-method s1 s2 x) (!fire (!fire subset-axiom [s1 s2]) [x])) ;; Transitivity of the subset relation: (define subset-trans (forall* [?s1 ?s2 ?s3] (if (and (subset ?s1 ?s2) (subset ?s2 ?s3)) (subset ?s1 ?s3)))) (!pf subset-trans [subset-axiom]) ;; A useful set-theory lemma: ;ALL s1,s2,s | (s1 subset s) /\ (s2 subset s) ==> (s1 union s2) subset s (define union-theorem-1 (forall* [?s1 ?s2 ?s] (if (and (subset ?s1 ?s) (subset ?s2 ?s)) (subset (union ?s1 ?s2) ?s)))) (!pf union-theorem-1 [subset-axiom union-axiom]) ;; Another useful result: ALL s1, s2, R | s1 subset s2 ==> (s1 . R) subset (s2 . R) (define dot-th' (pick-any s1 (pick-any s2 (pick-any R (assume-let ((hyp1 (subset s1 s2))) (dlet ((goal (if (in ?t (sbdot s1 R)) (in ?t (sbdot s2 R)))) (P (by-induction-on ?t goal ((cons y unit) (assume-let ((hyp2 (in (tup [y]) (sbdot s1 R)))) (!pf (in (tup [y]) (sbdot s2 R)) [hyp2 hyp1 subset-axiom sbdot-axiom])))))) (!pf (subset (sbdot s1 R) (sbdot s2 R)) [P subset-axiom]))))))) (define dot-th'' (pick-any s1 s2 R (assume ((hyp "s1 subset s2")) (dlet ((lemma (structure-cases "ALL t | t in s1.R ==> t in s2.R" ((cons y unit) (assume ((hyp' "[y] in s1.R")) (!pf "[y] in s2.R" [hyp hyp' subset-axiom sbdot-axiom])))))) (!pf (subset "s1.R" "s2.R") [lemma subset-axiom]))))) ;; Proves x = y from the assumption [x] in {[y]} (define (eq-tup-parts premise) (dmatch premise ((in (cons x unit) (singl (cons y unit))) (dlet ((P1 ((= (tup [x]) (tup [y])) BY (!fire singleton-axiom [(tup [x]) (tup [y])])))) (!left-and (!mp (!uspec* (!constructor-injectivity cons) [x unit y unit]) P1)))))) (define (eq-tup-parts1 premise) (dmatch premise ((in (cons x unit) (singl (cons y unit))) (!pf (= x y) [premise (!constructor-injectivity cons) singleton-axiom])))) ;; Another simple lemma: ALL x, y, R | [y] in ({[x]} . R) <==> [x y] in R (define sl (forall* [?x ?y ?R] (if (in (tup [?y]) (sbdot (scalar ?x) ?R)) (in (tup [?x ?y]) ?R)))) (!pf sl [sbdot-axiom singleton-axiom-1]) (pick-any x (pick-any y (pick-any R (assume-let ((hyp (in (tup [y]) (sbdot (scalar x) R)))) (dlet ((goal (exists ?x1 (and (in ?x1 (scalar x)) (in (tup [?x1 y]) R)))) (foo (begin (t goal) (print "\n") (t hyp) (print "\n") (t sbdot-axiom) (read))) (P (!pf [hyp sbdot-axiom]))) $P))))) (define scalar-lemma (pick-any x (pick-any y (pick-any R (dlet ((imp1 (assume-let ((hyp (in (tup [y]) (sbdot (scalar x) R)))) (dlet ((P ((exists ?X (and (in (tup [?X]) (scalar x)) (in (tup [?X y]) R))) BY (!fire sbdot-axiom [R (scalar x) y])))) (pick-witness X P (dlet ((P1 (replace-var (qvar-of P) X (body-of P))) (P2 (!left-and P1)) (P3 ((= X x) BY (!eq-tup-parts P2))) (P4 ((= (tup [X y]) (tup [x y])) BY (!rec-cong (tup [X y]) (tup [x y])))) (P5 (!right-and P1)) (P6 (!eq-reflex R))) ((in (tup [x y]) R) BY (!rel-cong-2 P5 [(tup [x y]) R]))))))) (imp2 (assume-let ((hyp (in (tup [x y]) R))) (dlet ((P1 ((in (tup [x]) (scalar x)) BY (!uspec singleton-axiom-1 (tup [x])))) (P2 (!both P1 hyp)) (P3 (!egen (exists ?foo (and (in (tup [?foo]) (scalar x)) (in (tup [?foo y]) R))) x))) (!fire sbdot-axiom [R (scalar x) y]))))) (!equiv imp1 imp2)))))) ;A useful lemma for power: ;; ALL x, y, z, R, k1, k2 | (x,y) in R^k1 /\ (y,z) in R^k2 ==> (x,z) in R^(k1+k2) (define power-sum-lemma (dlet ((goal (forall* [?x ?y ?z ?R ?k2] (if (and (holds (pow ?R ?k1) [?x ?y]) (holds (pow ?R ?k2) [?y ?z])) (holds (pow ?R (+ ?k1 ?k2)) [?x ?z]))))) (by-induction-on ?k1 goal (zero (pick-any x (pick-any y (pick-any z (pick-any R (pick-any k2 (assume-let ((hyp (and (holds (pow R zero) [x y]) (holds (pow R k2) [y z])))) (dlet ((P1 (!left-and hyp)) (P2 (!right-and hyp)) (- ((= y x) BY (!eq-symmetry2 (!fire pow-axiom-1 [R x y])))) (P3 ((holds (pow R k2) [x z]) BY (!substitute-equals y P2 x))) (P4 ((= k2 (+ zero k2)) BY (!eq-symmetry2 (!uspec plus-axiom-1 k2))))) (!substitute-equals k2 P3 (+ zero k2)))))))))) ((succ k) (pick-any x (pick-any y (pick-any z (pick-any R (pick-any k2 (dlet ((hyp (and (holds (pow R (succ k)) [x y]) (holds (pow R k2) [y z]))) (ihyp (forall* [x y z R k2] (if (and (holds (pow R k) [x y]) (holds (pow R k2) [y z])) (holds (pow R (+ k k2)) [x z]))))) (assume hyp (dlet ((P5 (!left-and hyp)) (P6 ((exists ?w (and (holds R [x ?w]) (holds (pow R k) [?w y]))) BY (!fire pow-axiom-2 [R k x y])))) (pick-witness w P6 (dlet ((P6-inst (replace-var (qvar-of P6) w (body-of P6))) (P7 ((holds (pow R k) [w y]) BY (!right-and P6-inst))) (P8 ((holds (pow R k2) [y z]) BY (!right-and hyp))) (P9 ((holds (pow R (+ k k2)) [w z]) BY (!fire ihyp [w y z R k2]))) (P10 (!both (!left-and P6-inst) P9)) (P10 (!egen (exists ?w (and (holds R [x ?w]) (holds (pow R (+ k k2)) [?w z]))) w)) (P11 ((holds (pow R (succ (+ k k2))) [x z]) BY (!fire pow-axiom-2 [R (+ k k2) x z]))) (P12 ((= (succ (+ k k2)) (+ (succ k) k2)) BY (!eq-symmetry2 (!uspec* plus-axiom-2 [k k2]))))) (!substitute-equals (succ (+ k k2)) P11 (+ (succ k) k2)))))))))))))))) ; Another lemma: ; ALL n, m | m in n.next* ==> m.next* subset n.next* (define comp-monotonicity (forall* [?n ?m ?R] (if (in (tup [?m]) (sbdot (scalar ?n) (rtc ?R))) (subset (sbdot (scalar ?m) (rtc ?R)) (sbdot (scalar ?n) (rtc ?R)))))) (pick-any n (pick-any m (pick-any R (assume (in (tup [m]) (sbdot (scalar n) (rtc R))) (dlet ((- ((holds (rtc R) [n m]) BY (!fire scalar-lemma [n m (rtc R)]))) (P1 ((exists ?k (holds (pow R ?k) [n m])) BY (!fire rtc-axiom [R n m])))) (pick-witness k P1 (dlet ((P1-inst (replace-var (qvar-of P1) k (body-of P1))) (goal (if (in ?v (sbdot (scalar m) (rtc R))) (in ?v (sbdot (scalar n) (rtc R))))) (P2 (by-induction-on ?v goal ((cons v unit) (assume-let ((hyp (in (tup [v]) (sbdot (scalar m) (rtc R))))) (dlet ((P3 ((in (tup [m v]) (rtc R)) BY (!fire scalar-lemma [m v (rtc R)]))) (P4 ((exists ?k (holds (pow R ?k) [m v])) BY (!fire rtc-axiom [R m v])))) (pick-witness k' P4 (dlet ((P4-inst (replace-var (qvar-of P4) k' (body-of P4))) (P5 (!both P1-inst P4-inst)) (P6 ((holds (pow R (+ k k')) [n v]) BY (!fire power-sum-lemma [k n m v R k']))) (P7 (!egen (exists ?s (holds (pow R ?s) [n v])) (+ k k'))) (P8 ((holds (rtc R) [n v]) BY (!fire rtc-axiom [R n v])))) (!fire scalar-lemma [n v (rtc R)]))))))))) (!fire subset-axiom [(sbdot (scalar m) (rtc R)) (sbdot (scalar n) (rtc R))])))))))) (!claim comp-monotonicity) ; Lemma: ALL n, R | (n,n) in R^0 (define rtc-zero-lemma (pick-any n (pick-any R (dlet ((P1 (!eq-reflex n))) ((in (tup [n n]) (pow R zero)) BY (!fire pow-axiom-1 [R n n])))))) ; Lemma: ALL n, R | (n,n) in R* (define reflex-clos-lemma (pick-any n (pick-any R (dlet ((P1 (!eq-reflex n)) (P2 ((in (tup [n n]) (pow R zero)) BY (!fire pow-axiom-1 [R n n]))) (P3 (!egen (exists ?k (holds (pow R ?k) [n n])) zero))) (!fire rtc-axiom [R n n]))))) ;; Another simple lemma: ALL x, y, R | (x,y) in R ==> (x,y) in R^1 (define first-power-lemma (pick-any x (pick-any y (pick-any R (assume-let ((hyp (holds R [x y]))) (dlet ((P1 ((holds (pow R zero) [y y]) BY (!uspec* rtc-zero-lemma [y R]))) (P2 (!both hyp P1)) (P3 (!egen (exists ?z (and (holds R [x ?z]) (holds (pow R zero) [?z y]))) y))) (!fire pow-axiom-2 [R zero x y]))))))) ;; And a similar one: ALL x, y, R | (x,y) in R ==> (x,y) in R^* (define first-power-lemma-1 (pick-any x (pick-any y (pick-any R (assume-let ((hyp (holds R [x y]))) (dlet ((P1 ((holds (pow R (succ zero)) [x y]) BY (!fire first-power-lemma [x y R]))) (P2 (!egen (exists ?k (holds (pow R ?k) [x y])) (succ zero)))) (!fire rtc-axiom [R x y]))))))) ; Prove: ALL n, R | {(n)} subset n.R* (define subset-ref-lemma (pick-any n (pick-any R (dlet ((P (by-induction-on ?x (if (in ?x (scalar n)) (in ?x (sbdot (scalar n) (rtc R)))) ((cons x unit) (assume (in (tup [x]) (scalar n)) (dlet ((P1 ((= n x) BY (!eq-symmetry2 (!eq-tup-parts (in (tup [x]) (scalar n)))))) (P2 ((in (tup [n n]) (rtc R)) BY (!uspec* reflex-clos-lemma [n R]))) (P3 ((in (tup [n]) (sbdot (scalar n) (rtc R))) BY (!fire scalar-lemma [n n (rtc R)])))) (!rec-rel-cong P3 (in (tup [x]) (sbdot (scalar n) (rtc R)))))))))) (!fire subset-axiom [(scalar n) (sbdot (scalar n) (rtc R))]))))) (define lemma-L1 (pick-any n (dlet ((P1 (!uspec* subset-ref-lemma [n next])) (P2 (!fire dot-th [(scalar n) (sbdot (scalar n) (rtc next)) data]))) $P2))) (define (exp1 n) (sbdot (scalar n) (rtc next))) (define (exp2 n) (sbdot (exp1 n) data)) (define (ind-goal n) (subset (elms n) (exp2 n))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (define base-step (pick-any n (assume-let ((hyp (not (exists ?m (holds next [n ?m]))))) (dlet ((P1 ((= (elms n) (sbdot (scalar n) data)) BY (!mp (!left-and (!uspec elms-semantics n)) hyp))) (P2 (!uspec lemma-L1 n))) (!rec-rel-cong P2 (subset (elms n) (sbdot (sbdot (scalar n) (rtc next)) data))))))) (define ind-step (pick-any n (pick-any m (assume-let ((hyp (holds next [n m])) (ihyp (ind-goal m))) (dlet ((P1 ((= (elms n) (union (sbdot (scalar n) data) (elms m))) BY (!mp (!uspec (!right-and (!uspec elms-semantics n)) m) hyp))) (P2 ((holds (rtc next) [n m]) BY (!fire first-power-lemma-1 [n m next]))) (P3 ((in (tup [m]) (sbdot (scalar n) (rtc next))) BY (!fire scalar-lemma [n m (rtc next)]))) (P4 ((subset (exp1 m) (exp1 n)) BY (!fire comp-monotonicity [n m next]))) (P5 ((subset (exp2 m) (exp2 n)) BY (!fire dot-th [(exp1 m) (exp1 n) data]))) (P6 ((subset (elms m) (exp2 n)) BY (!fire subset-trans [(elms m) (exp2 m) (exp2 n)]))) (P7 ((subset (sbdot (scalar n) data) (exp2 n)) BY (!uspec lemma-L1 n))) (P8 ((subset (union (sbdot (scalar n) data) (elms m)) (exp2 n)) BY (!fire union-theorem-1 [(sbdot (scalar n) data) (elms m) (exp2 n)])))) (!rec-rel-cong P8 (subset (elms n) (exp2 n)))))))) (assert acyclicity) (define inductive-proof (!list-induction ind-goal)) ; (load-file "elms2.ath") ; (load-file "elm-lemmas.ath") ; (load-file "elms-proofs.ath") ;