commit

Author: Hakerh400

src/index.js

@@ -12,7 +12,7 @@ const ident2sym = require('./ident2sym');
 const Expr = require('../theorems/expr');
 const debug = require('./debug');
 
-const PRETTY_LOG = 1;
+const PRETTY_LOG = 0;
 
 const {tilde} = parser;
 const {isSym, isPair} = database;
@@ -98,7 +98,7 @@ const verify = (thName, force=0, db=null) => {
         args.length !== 0 ? ` --- ${
           args.map(arg => info2str(arg)).join(`,${
           ' '.repeat(2)}`)}` : ''}`;
-    }).join('\n');
+    }).join('\n\n');
   };
 
   const reduce = function*(info){
@@ -122,7 +122,10 @@ const verify = (thName, force=0, db=null) => {
       return db.reduceToItself(info);
 
     const err = msg => {
-      error(`${msg}\n\n${info2str(info)}\n\n${getStackTrace()}`);
+      log(`${msg}\n\n${info2str(info)}`);
+      O.logb();
+      log(getStackTrace());
+      O.exit();
     };
 
     const {cases} = func;
@@ -350,8 +353,10 @@ const info2str = info => {
         return `~${a}`;
       }
 
-      if(op === 'Proof')
-        return O.tco(info2str, expr[1]);
+      if(op === 'Proof'){
+        const a = yield [info2str, expr[1], 1];
+        return `|- ${a}`;
+      }
     }
 
     if(isSym(expr))

system/core/funcs/assert.drift

@@ -1,3 +1,5 @@
 assert True = id
 
-assertEq a b = assert (eq a b)
+assert.fail = assert false
+
+assert.eq a b = assert (eq a b)

system/core/types/proof.drift

@@ -4,10 +4,10 @@ Proof:
 
   rule.mp (Proof (Impl a b)) (Proof a) = Proof b
 
-  rule.uni.intr_ (Proof (Impl a b)) (Nat c) = assert (not (hasIdent c a))
+  rule.uni.intr_ (Nat c) (Proof (Impl a b)) = assert (not (hasIdent c a))
     (Proof (impl a (forall c b)))
 
-  rule.uni.elim_ (Proof (Impl a (Forall b c))) (Nat d) =
+  rule.uni.elim_ (Nat d) (Proof (Impl a (Forall b c))) =
     Proof (impl a (substIdentStrict b d c))
 
   ax.prop.1 = Proof (impl phi (impl psi phi))
@@ -19,5 +19,5 @@ Proof:
   ax.prop.3 = Proof (impl (impl (pnot phi) (pnot psi)) (impl psi phi))
 
 rule.inst a b c = rule.inst_ a b (pred c)
-rule.uni.intr a b = rule.uni.intr_ a (nat b)
-rule.uni.elim a b = rule.uni.elim_ a (nat b)
+rule.uni.intr a b = rule.uni.intr_ (nat a) b
+rule.uni.elim a b = rule.uni.elim_ (nat a) b

system/funcs/pred.drift

@@ -1,4 +1,26 @@
 implr a = impl a a
 
 iff = synt.iff
-iffr a = iff a a
+iffr a = iff a a
+
+op2pair func pred = op2pair_opPair (func phi psi) pred (pair nil nil)
+op2pair_opPair &phi pred (Pair Nil a) = pair pred a
+op2pair_opPair &phi pred (Pair pred a) = pair pred a
+op2pair_opPair &psi pred (Pair a Nil) = pair a pred
+op2pair_opPair &psi pred (Pair a pred) = pair a pred
+op2pair_opPair (Impl a1 b1) (Impl a2 b2) opPair = op2pair_opPair b1 b2 (op2pair_opPair a1 a2 opPair)
+op2pair_opPair (Pnot a1) (Pnot a2) opPair = op2pair_opPair a1 a2 opPair
+op2pair_opPair (Forall a b1) (Forall a b2) opPair = op2pair_opPair b1 b2 opPair
+op2pair_opPair (Pelem a b) (Pelem a b) opPair = opPair
+
+impl2pair (Impl a b) = pair a b
+or2pair = op2pair synt.or
+and2pair = op2pair synt.and
+iff2pair = op2pair iff
+
+hasSubPred sub sub = true
+hasSubPred sub (Pident *) = false
+hasSubPred sub (Impl a b) = or (hasSubPred sub a) (hasSubPred sub b)
+hasSubPred sub (Pnot a) = hasSubPred sub a
+hasSubPred sub (Forall * a) = hasSubPred sub a
+hasSubPred sub (Pelem * *) = false

system/theorems/prop/basic.drift

@@ -256,4 +256,18 @@ th.prop.a.-a.b_ a = util.addSup2 a
   (pnot phi)
 
 -- ~a -> a -> b
-th.prop.-a.a.b = util.reord th.prop.a.-a.b
+th.prop.-a.a.b = util.reord th.prop.a.-a.b
+
+-- T <-> Ɐa (a = a)
+th.true.def = prove.taut
+  (synt.iff synt.true (forall a. (synt.eq a. a.)))
+
+-- ⊥ <-> ~T
+th.false.def = prove.taut
+  (synt.iff synt.false (pnot synt.true))
+
+-- T
+th.true = prove.taut synt.true
+
+-- ~⊥
+th.nfalse = prove.taut (pnot synt.false)

system/theorems/prop/eq.drift

@@ -1,31 +1,47 @@
 -- Ɐa Ɐb (a = b <-> Ɐc (c ∈ a <-> c ∈ b) ^ Ɐc (a ∈ c <-> b ∈ c))
-th.eq.def = util.uni.intr
-  (util.uni.intr
-    (util.iff.refl (synt.eq a. b.))
-    b.)
-  a.
+th.eq.def = util.uni.intr a.
+  (util.uni.intr b.
+    (util.iff.refl (synt.eq a. b.)))
 
 -- Ɐa (a = a)
-th.eq.refl = util.uni.intr
+th.eq.refl = util.uni.intr a.
   (util.and
-    (util.uni.intr
-      (util.iff.refl (pelem b. a.))
-      b.)
-    (util.uni.intr
-      (util.iff.refl (pelem a. b.))
-      b.))
-  a.
+    (util.uni.intr b.
+      (util.iff.refl (pelem b. a.)))
+    (util.uni.intr b.
+      (util.iff.refl (pelem a. b.))))
 
--- T <-> Ɐa (a = a)
-th.true.def = prove.taut
-  (synt.iff synt.true (forall a. (synt.eq a. a.)))
+----------------------------------------------------------------------------------------------------
 
--- ⊥ <-> ~T
-th.false.def = prove.taut
-  (synt.iff synt.false (pnot synt.true))
-
--- T
-th.true = prove.taut synt.true
-
--- ~⊥
-th.nfalse = prove.taut (pnot synt.false)
+-- th_a = id
+--   (util.and
+--     (util.uni.intr b.
+--       (util.iff.refl (pelem b. a.)))
+--     (util.uni.intr b.
+--       (util.iff.refl (pelem a. b.))))
+-- 
+-- th_b = id
+--   (util.and
+--     (util.uni.intr a.
+--       (util.iff.refl (pelem a. b.)))
+--     (util.uni.intr a.
+--       (util.iff.refl (pelem b. a.))))
+-- 
+-- iff_ab = util.infer2
+--   (prove.taut (impl phi
+--     (impl psi (synt.iff phi psi))))
+--   th_a
+--   th_b
+-- 
+-- th1 = util.uni.intr c.
+--   (util.infer
+--     (rule.inst
+--       (prove.taut (impl phi (synt.or phi psi)))
+--       psi (pelem c. d.))
+--     th_a)
+-- 
+-- test = rule.mp
+--   (util.infer
+--     th.prop.iff.def.2
+--     (util.subst (extract th1) iff_ab))
+--   th1

system/util/prop.drift

@@ -39,6 +39,14 @@ util.infer proofImpl:(Proof (Impl a b)) proofPremise = rule.mp
   (util.inst proofImpl (autoPidentPredPairs a (extract proofPremise)))
   proofPremise
 
+util.infer2 proofImpl proofPrem1 proofPrem2 = util.infer
+  (util.infer proofImpl proofPrem1)
+  proofPrem2
+
+util.infer3 proofImpl proofPrem1 proofPrem2 proofPrem3 = util.infer
+  (util.infer2 proofImpl proofPrem1 proofPrem2)
+  proofPrem3
+
 util.infer.ax2 = util.infer th.prop.ax2
 util.infer.ax3 = util.infer th.prop.ax3
 util.infer.mpt = util.infer th.prop.mpt

system/util/quant.drift

@@ -1,9 +1,8 @@
-util.uni.intr proof:(Proof pred) ident =
-  util.uni.intr_ proof ident (availIdent pred)
-util.uni.intr_ proof ident avail = rule.mp
-  (rule.uni.intr
+util.uni.intr ident proof:(Proof pred) =
+  util.uni.intr_ ident (availIdent pred) proof
+util.uni.intr_ ident avail proof = rule.mp
+  (rule.uni.intr ident
     (util.addSup
       proof
-      (implr (pelem avail avail)))
-    ident)
+      (implr (pelem avail avail))))
   (util.impl.refl (pelem avail avail))

system/util/subst.drift

@@ -1 +1,54 @@
-util.subst = id
+-- Given a predicate `pred` and a proof of `pred1 <-> pred2`
+-- Prove that `pred <-> pred_` where `pred_` is `pred` with
+-- all occurences of `pred1` replaced with `pred2`
+
+util.subst pred proof:(Proof predIff) = callWithPair
+  (util.subst_preds proof) (iff2pair predIff) pred
+
+-- Optimization
+util.subst_preds proof pred1 pred2 pred = ite (hasSubPred pred1 pred)
+  (util.subst_preds_raw proof pred1 pred2) util.iff.refl pred
+
+util.subst_preds_raw proof pred1 pred2 pred1 = proof
+util.subst_preds_raw proof pred1 pred2 pident:(Pident *) = util.iff.refl pident
+util.subst_preds_raw proof pred1 pred2 (Impl a b) = util.infer2
+  (prove.taut
+    (impl (synt.iff phi chi) (impl
+      (synt.iff psi theta) (synt.iff
+        (impl phi psi)
+        (impl chi theta)))))
+  (util.subst_preds proof pred1 pred2 a)
+  (util.subst_preds proof pred1 pred2 b)
+util.subst_preds_raw proof pred1 pred2 (Pnot a) = util.infer
+  (prove.taut
+    (impl (synt.iff phi psi) (synt.iff
+      (pnot phi)
+      (pnot psi))))
+  (util.subst_preds proof pred1 pred2 a)
+util.subst_preds_raw proof pred1 pred2 pelem:(Forall ident pred) = callWithPair
+  (util.subst_preds_forall
+    ident
+    (util.subst_preds proof pred1 pred2 pred))
+  (iff2pair (extract (util.subst_preds proof pred1 pred2 pred)))
+util.subst_preds_raw proof pred1 pred2 pelem:(Pelem * *) = util.iff.refl pelem
+
+util.subst_preds_forall ident proof p1 p2 = util.infer2
+  th.prop.iff.def.1
+  (util.subst_preds_forall_impl
+    ident
+    (util.infer
+      th.prop.iff.def.2
+      proof)
+    p1)
+  (util.subst_preds_forall_impl
+    ident
+    (util.infer
+      th.prop.iff.def.3
+      proof)
+    p2)
+
+util.subst_preds_forall_impl ident proof pred = rule.uni.intr ident
+  (util.tran
+    (rule.uni.elim ident
+      (util.impl.refl (forall ident pred)))
+    proof)