Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP

Comparing changes

Choose two branches to see what's changed or to start a new pull request. If you need to, you can also compare across forks.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also compare across forks.
base fork: ezyang/logitext
base: 425df7ff6a
...
head fork: ezyang/logitext
compare: 0bc8d5983d
Checking mergeability… Don't worry, you can still create the pull request.
  • 2 commits
  • 3 files changed
  • 0 commit comments
  • 1 contributor
Commits on May 20, 2012
@ezyang Manually add support for contract.
Signed-off-by: Edward Z. Yang <ezyang@mit.edu>
944c019
@ezyang Fix line-wrapping, remove print, prettify.
Signed-off-by: Edward Z. Yang <ezyang@mit.edu>
0bc8d59
Showing with 28 additions and 19 deletions.
  1. +0 −1  ClassicalFOLFFI.hs
  2. +26 −16 logitext.ur
  3. +2 −2 style.css
View
1  ClassicalFOLFFI.hs
@@ -65,7 +65,6 @@ refineFFI ctx s = serialize ctx $ do
lazyByteStringToUrWebCString ctx bs = do
let s = S.concat (L.toChunks bs)
- print s
-- XXX S.concat is really bad! Bad Edward!
S.unsafeUseAsCStringLen s $ \(c,n) -> do
x <- uw_malloc ctx (n+1)
View
42 logitext.ur
@@ -120,8 +120,8 @@ fun tacticRenderName [a] (t : tactic a) : string = match t
, LNot = fn _ => "(¬l)"
, LForall = fn _ => "(∀l)"
, LExists = fn _ => "(∃l)"
- , LContract = fn _ => "(contract:l)"
- , LWeaken = fn _ => "(weaken:l)"
+ , LContract = fn _ => ""
+ , LWeaken = fn _ => ""
, RExact = fn _ => ""
, RConj = fn _ => "(∧r)"
, RDisj = fn _ => "(∨r)"
@@ -131,8 +131,8 @@ fun tacticRenderName [a] (t : tactic a) : string = match t
, RNot = fn _ => "(¬r)"
, RForall = fn _ => "(∀r)"
, RExists = fn _ => "(∃r)"
- , RContract = fn _ => "(contract:r)"
- , RWeaken = fn _ => "(weaken:r)"
+ , RContract = fn _ => ""
+ , RWeaken = fn _ => ""
}
con end_user_failure = variant [UpdateFailure = unit, ParseFailure = unit]
@@ -156,7 +156,7 @@ end)
type proof = Proof.r
fun renderSequent (h : proof -> transaction unit) (s : sequent) : transaction xbody =
let fun makePending (x : tactic int) : transaction unit = h (Proof.Rec (make [#Pending] (s, x)))
- fun makePendingU prompter (f : universe -> tactic int) : transaction unit =
+ fun makePendingU prompter (f : universe -> tactic int) (g : tactic int) : transaction unit =
r <- source "";
(* XXX would be nice if the ctextbox automatically grabbed focus *)
set prompter <xml><div class={relMark}>
@@ -173,6 +173,8 @@ fun renderSequent (h : proof -> transaction unit) (s : sequent) : transaction xb
})
else return ()}
onblur={set prompter <xml></xml>} />
+ or
+ <button value="Contract" onclick={makePending g} />
</div>
</div></xml>
in
@@ -187,7 +189,7 @@ fun renderSequent (h : proof -> transaction unit) (s : sequent) : transaction xb
Not = fn _ => makePending (make [#LNot] (i, 0)),
Top = fn _ => makePending (make [#LTop] (i, 0)),
Bot = fn _ => makePending (make [#LBot] i),
- Forall = fn _ => makePendingU prompter (fn u => make [#LForall] (i, u, 0)),
+ Forall = fn _ => makePendingU prompter (fn u => make [#LForall] (i, u, 0)) (make [#LContract] (i, 0)),
Exists = fn _ => makePending (make [#LExists] (i, 0))
}}>
{renderLogic 0 (Logic.Rec x)}</span><dyn signal={signal prompter}/></li></xml>) s.Hyps;
@@ -202,7 +204,7 @@ fun renderSequent (h : proof -> transaction unit) (s : sequent) : transaction xb
Top = fn _ => makePending (make [#RTop] i),
Bot = fn _ => makePending (make [#RBot] (i, 0)),
Forall = fn _ => makePending (make [#RForall] (i, 0)),
- Exists = fn _ => makePendingU prompter (fn u => make [#RExists] (i, u, 0)),
+ Exists = fn _ => makePendingU prompter (fn u => make [#RExists] (i, u, 0)) (make [#RContract] (i, 0)),
}}>
{renderLogic 0 (Logic.Rec x)}</span><dyn signal={signal prompter}/></li></xml>) s.Cons;
return <xml><ul class={commaList}>{left}</ul> ⊢ <ul class={commaList}>{right}</ul></xml>
@@ -333,6 +335,8 @@ fun tutorial () =
exOrIdentity <- mkWorkspace "A \/ B |- B \/ A";
exDeMorgan <- mkWorkspace "~(A \/ B) -> ~A /\ ~B";
exForallDist <- mkWorkspace "(forall x. P(x)) /\ (forall x. Q(x)) -> forall y. P(y) /\ Q(y)";
+ exForallContract <- mkWorkspace "forall x. (P(x)->P(f(x))) |- forall x. (P(x) -> P(f(f(x))))";
+ solvedForallContract <- mkExample "{\"Success\":{\"Proof\":{\"1\":{\"cons\":[{\"Forall\":{\"1\":\"x\",\"2\":{\"Imp\":{\"1\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"x\",\"2\":[]}]}},\"2\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}]}}}}}}],\"hyps\":[{\"Forall\":{\"1\":\"x\",\"2\":{\"Imp\":{\"1\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"x\",\"2\":[]}]}},\"2\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}}}}}}]},\"2\":{\"LContract\":{\"1\":0,\"2\":{\"Proof\":{\"1\":{\"cons\":[{\"Forall\":{\"1\":\"x\",\"2\":{\"Imp\":{\"1\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"x\",\"2\":[]}]}},\"2\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}]}}}}}}],\"hyps\":[{\"Forall\":{\"1\":\"x\",\"2\":{\"Imp\":{\"1\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"x\",\"2\":[]}]}},\"2\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}}}}}},{\"Forall\":{\"1\":\"x\",\"2\":{\"Imp\":{\"1\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"x\",\"2\":[]}]}},\"2\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}}}}}}]},\"2\":{\"RForall\":{\"1\":0,\"2\":{\"Proof\":{\"1\":{\"cons\":[{\"Imp\":{\"1\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"x\",\"2\":[]}]}},\"2\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}]}}}}],\"hyps\":[{\"Forall\":{\"1\":\"x\",\"2\":{\"Imp\":{\"1\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"x\",\"2\":[]}]}},\"2\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}}}}}},{\"Forall\":{\"1\":\"x\",\"2\":{\"Imp\":{\"1\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"x\",\"2\":[]}]}},\"2\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}}}}}}]},\"2\":{\"RImp\":{\"1\":0,\"2\":{\"Proof\":{\"1\":{\"cons\":[{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}]}}],\"hyps\":[{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"x\",\"2\":[]}]}},{\"Forall\":{\"1\":\"x\",\"2\":{\"Imp\":{\"1\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"x\",\"2\":[]}]}},\"2\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}}}}}},{\"Forall\":{\"1\":\"x\",\"2\":{\"Imp\":{\"1\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"x\",\"2\":[]}]}},\"2\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}}}}}}]},\"2\":{\"LForall\":{\"1\":1,\"3\":{\"Proof\":{\"1\":{\"cons\":[{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}]}}],\"hyps\":[{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"x\",\"2\":[]}]}},{\"Imp\":{\"1\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"x\",\"2\":[]}]}},\"2\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}}}},{\"Forall\":{\"1\":\"x\",\"2\":{\"Imp\":{\"1\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"x\",\"2\":[]}]}},\"2\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}}}}}}]},\"2\":{\"LImp\":{\"1\":1,\"3\":{\"Proof\":{\"1\":{\"cons\":[{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}]}}],\"hyps\":[{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"x\",\"2\":[]}]}},{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}},{\"Forall\":{\"1\":\"x\",\"2\":{\"Imp\":{\"1\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"x\",\"2\":[]}]}},\"2\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}}}}}}]},\"2\":{\"LForall\":{\"1\":2,\"3\":{\"Proof\":{\"1\":{\"cons\":[{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}]}}],\"hyps\":[{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"x\",\"2\":[]}]}},{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}},{\"Imp\":{\"1\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}},\"2\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}]}}}}]},\"2\":{\"LImp\":{\"1\":2,\"3\":{\"Proof\":{\"1\":{\"cons\":[{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}]}}],\"hyps\":[{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"x\",\"2\":[]}]}},{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}},{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}]}}]},\"2\":{\"LExact\":2}}},\"2\":{\"Proof\":{\"1\":{\"cons\":[{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}},{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}]}}],\"hyps\":[{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"x\",\"2\":[]}]}},{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}}]},\"2\":{\"LExact\":1}}}}}}},\"2\":{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}}}}},\"2\":{\"Proof\":{\"1\":{\"cons\":[{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"x\",\"2\":[]}]}},{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}]}}],\"hyps\":[{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"x\",\"2\":[]}]}},{\"Forall\":{\"1\":\"x\",\"2\":{\"Imp\":{\"1\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"x\",\"2\":[]}]}},\"2\":{\"Pred\":{\"1\":\"P\",\"2\":[{\"1\":\"f\",\"2\":[{\"1\":\"x\",\"2\":[]}]}]}}}}}}]},\"2\":{\"RExact\":0}}}}}}},\"2\":{\"1\":\"x\",\"2\":[]}}}}}}}}}}}}}}}}}}";
return <xml>
<head>
<title>Tutorial</title>
@@ -342,7 +346,7 @@ fun tutorial () =
infAxiom.Onload; infLConj.Onload; infRConj.Onload; infLImp.Onload; infRImp.Onload;
infLDisj.Onload; infRDisj.Onload; infLNot.Onload; infRNot.Onload; infLForall.Onload; infRForall.Onload;
infLExists.Onload; infRExists.Onload; exForallIdentity.Onload; exAndIdentity.Onload; exOrIdentity.Onload;
- exDeMorgan.Onload; exForallDist.Onload
+ exDeMorgan.Onload; exForallDist.Onload; exForallContract.Onload
}>
<div class={page}>
@@ -481,7 +485,7 @@ fun tutorial () =
<p>The rules for the quantifiers are particularly interesting. The
left and right rules look symmetrical, but there's an important difference:
in the case of a the left-forall rule, you (the prover) get to pick what
- to replace <i>x</i> with. In the right-forall rule, the system picks a
+ to replace <i>x</i> with (ignore the button that says "Contract" for now). In the right-forall rule, the system picks a
variable that doesn't match anything you've seen before. (In the case
of exists, the situation is swapped.) This is important if you
want to prove this statement:</p>
@@ -499,18 +503,25 @@ fun tutorial () =
it's a good idea to have the system pick as many variables for you as
possible, before you do any choosing.</p>
+ <p>The final piece of the puzzle is the "contract" button, which
+ duplicates a hypothesis or goal, so you can reuse it later. Use
+ of this <i>structural rule</i> may be critical to certain proofs.</p>
+
<p>With these inference rules, you now have the capability to
- prove almost everything in first-order logic! (The one last inference
- rule you need is called contraction, but I haven't implemented
- the interface for it.) The next section will contain some exercises
+ prove everything in first-order logic! The next section will contain some exercises
for you to try.</p>
<h2>Exercises</h2>
+ <p>Nota bene: the last one requires contraction.</p>
+
{exAndIdentity.Widget}
{exOrIdentity.Widget}
{exDeMorgan.Widget}
{exForallDist.Widget}
+ {exForallContract.Widget}
+
+ <p>Return to <a link={main ()}>the main page.</a></p>
</div>
</body>
@@ -530,8 +541,9 @@ and proving goal =
on sequents. Inference rules correspond closely to <i>clauses</i> in the sequent,
so in Logitext (and other proof-by-pointing systems), all you need to do is click
on a clause to see what inference rule is triggered (some rules will need a
- member of the universe (e.g. <i>z</i>), in which case an input box will pop up.
- If that made no sense to use, check out <a link={tutorial ()}>the tutorial</a>.
+ member of the universe, try using <i>z</i>), in which case an input box will pop up
+ (you can also choose to duplicate the rules by clicking "Contract").
+ If that made no sense to you, check out <a link={tutorial ()}>the tutorial</a>.
Or, you can <a link={main ()}>return to main page...</a></p>
</div>
{wksp.Widget}
@@ -585,8 +597,6 @@ and main () =
<li>z : U (our universe is non-empty, so z is always a valid member
of the universe)</li>
</ul>
- <p>Unfortunately, we don't currently support contraction/weakening rules,
- so there may be some statements you cannot prove yet.</p>
</div>
</body>
</xml>
View
4 style.css
@@ -6,7 +6,7 @@ h2 { font-family:sans-serif; font-size:1.3em; border-bottom:1px solid #BBB; }
.viewport { height:500px; width:800px; overflow:hidden; border:1px #CCC solid; text-align:center; }
.working { text-align:center; margin-top:1em; }
-.proof { display:inline-block; }
+.proof { display:inline-block; white-space:nowrap; }
.proof table { width:100%; border-collapse:collapse; margin: auto; }
.proof td { padding:0; border:0; margin:0; text-align:center; }
.proof .sibling { display: inline-block; vertical-align:bottom; }
@@ -23,7 +23,7 @@ h2 { font-family:sans-serif; font-size:1.3em; border-bottom:1px solid #BBB; }
/* hat tip http://stackoverflow.com/questions/6040005/relatively-position-an-element-without-it-taking-up-space-in-document-flow */
.relMark {position:relative; width:0; height:0; display:inline;}
-.offsetBox {position:absolute; z-index:1; top:1em; left:0;}
+.offsetBox {position:absolute; z-index:1; top:1em; left:0; background:#FFF; width:13em;}
.error {margin-top:1em; border:1px solid #900; padding:0.2em; background: #F99; }

No commit comments for this range

Something went wrong with that request. Please try again.