[guru-lang] r547 committed - Added UnjoinBase, a class containing common functionality between Unjo...
guru...@googlecode.com
Author: kevinclancy0
Date: Mon Nov 14 12:52:03 2011
Log: Added UnjoinBase, a class containing common functionality between
Unjoin and UnjoinContra.
Fixed bugs, added match lifting and non-unfolding evaluation.
http://code.google.com/p/guru-lang/source/detail?r=547
Added:
/branches/1.0/guru/UnjoinBase.java
Modified:
/branches/1.0/guru/Const.java
/branches/1.0/guru/Expr.java
/branches/1.0/guru/LemmaSet.java
/branches/1.0/guru/Let.java
/branches/1.0/guru/Match.java
/branches/1.0/guru/TermApp.java
/branches/1.0/guru/Unjoin.java
/branches/1.0/guru/UnjoinContext.java
/branches/1.0/guru/UnjoinContra.java
/branches/1.0/guru/Var.java
/branches/1.0/tests/unjoin.g
=======================================
--- /dev/null
+++ /branches/1.0/guru/UnjoinBase.java Mon Nov 14 12:52:03 2011
@@ -0,0 +1,621 @@
+package guru;
+
+import java.io.PrintStream;
+import java.util.List;
+import java.util.Stack;
+import java.util.Vector;
+
+public abstract class UnjoinBase extends Expr {
+
+ // An expression which proves the scrutinee atom.
+ public final Expr scrutineeProof;
+
+ public UnjoinBase(int construct, Expr scrutineeProof)
+ {
+ super(construct);
+
+ assert(scrutineeProof != null);
+ assert(construct == UNJOIN || construct == UNJOIN_CONTRA);
+
+ this.scrutineeProof = scrutineeProof;
+ }
+
+ public static boolean placeHolder(Expr e, Context ctxt)
+ {
+ if (e.construct == VAR)
+ return true;
+
+ if (e.construct == CONST && e.evalStep(ctxt) != e)
+ return true;
+
+ return false;
+ }
+
+ //Non-unfolding evaluation step
+ public Expr nustep(Expr e, Context ctxt)
+ {
+ switch (e.construct)
+ {
+ case Expr.TERM_APP:
+ TermApp ta = (TermApp)e;
+
+ Expr h = ta.head;
+ if (h.construct != CONST) {
+ h = nustep(h, ctxt);
+
+ if (h != ta.head) {
+ Expr ret = new TermApp(h, ta.X);
+ ret.pos = pos;
+ return ret;
+ }
+ }
+
+ if (h.construct == ABORT)
+ //return ctxt.abort;
+ return h;
+
+ int iend = ta.X.length;
+ Expr[] X2 = new Expr[iend];
+ for (int i = 0; i < iend; i++) {
+ X2[i] = nustep(ta.X[i], ctxt);
+ if (X2[i] != ta.X[i]) {
+ for (int j = i+1; j < iend; j++)
+ X2[j] = ta.X[j];
+ Expr ret = new TermApp(h, X2);
+ ret.pos = pos;
+ return ret;
+ }
+ else if (ta.X[i].construct == ABORT) {
+ //return ctxt.abort;
+ return ta.X[i];
+ }
+ }
+
+ // none of the args evaluated to something different
+ if (h.construct != FUN_TERM)
+ return e;
+
+ FunTerm f = (FunTerm)h;
+
+ // We do not instantiate recursive functions to avoid
+ // explosion.
+ if (f.r != null)
+ return e;
+
+ iend = X2.length;
+
+ Expr hh = f.substituteForParam(X2[0]);
+ if (iend == 1)
+ return hh;
+
+ iend--;
+ Expr[] X3 = new Expr[iend];
+ for (int i = 0; i < iend; i++)
+ X3[i] = X2[i+1];
+ Expr ret = new TermApp(hh, X3);
+ ret.pos = pos;
+ return ret;
+ case Expr.FUN_TERM:
+ return e;
+ case Expr.VAR:
+ return e.defExpandTop(ctxt);
+ case Expr.CONST:
+ return e;
+ case Expr.MATCH:
+ return e;
+ case Expr.BANG:
+ return e;
+ case Expr.DO:
+ Do d = (Do)e;
+ return d.t;
+ case Expr.VOIDI:
+ return e;
+ case Expr.LET:
+ Let l = (Let)e;
+ Expr et1 = nustep(l.t1, ctxt);
+ if (et1 != l.t1)
+ return new Let(l.x1, l.x1_stat, et1, l.x2, l.t2);
+ if (l.t1.construct == ABORT)
+ return l.t1;
+ return l.t2.subst(l.t1, l.x1);
+ default:
+ assert(false);
+ return null;
+ }
+ }
+
+ public Expr nueval(Expr e, Context ctxt)
+ {
+ Expr e2 = e;
+
+ while (e2 != nustep(e2,ctxt))
+ {
+ System.out.println(e2.toString(ctxt));
+ e2 = nustep(e2,ctxt);
+ }
+
+ return e2;
+ }
+
+ class LiftedMatch
+ {
+ public final Expr scrut;
+ public final Var hole;
+ public final Case[] cases;
+ public final Expr context;
+
+ public LiftedMatch(Expr scrut, Var hole, Case[] cases, Expr context) {
+ assert(matchFree(scrut));
+
+ for (int i = 0; i < cases.length; ++i) {
+ assert(cases[i] != null);
+ assert(matchFree(cases[i].body));
+ }
+
+ this.scrut = scrut;
+ this.hole = hole;
+ this.cases = cases;
+ this.context = context;
+ }
+ }
+
+ public LiftedMatch liftSingleMatch(Expr e)
+ {
+ switch (e.construct)
+ {
+ case Expr.TERM_APP:
+ TermApp ta = (TermApp)e;
+
+ LiftedMatch lift = liftSingleMatch(ta.head);
+ if (lift != null)
+ {
+ return new LiftedMatch(
+ lift.scrut,
+ lift.hole,
+ lift.cases,
+ new TermApp(lift.context, ta.X)
+ );
+ }
+
+ for (int i = 0; i < ta.X.length; ++i) {
+ lift = liftSingleMatch(ta.X[i]);
+ if (lift != null) {
+ Expr[] X2 = new Expr[ta.X.length];
+
+ for (int j = 0; j < ta.X.length; ++j)
+ {
+ if (i == j)
+ X2[j] = lift.context;
+ else
+ X2[j] = ta.X[j];
+ }
+
+ return new LiftedMatch(
+ lift.scrut,
+ lift.hole,
+ lift.cases,
+ new TermApp(ta.head, X2)
+ );
+ }
+ }
+
+ return null;
+ case Expr.FUN_TERM:
+ return null;
+ case Expr.VAR:
+ return null;
+ case Expr.CONST:
+ return null;
+ case Expr.BANG:
+ return null;
+ case Expr.VOIDI:
+ return null;
+ case Expr.MATCH:
+ Match m = (Match)e;
+
+ lift = liftSingleMatch(m.t);
+
+ if (lift != null) {
+ return new LiftedMatch(
+ lift.scrut,
+ lift.hole,
+ lift.cases,
+ new Match(
+ lift.context,
+ m.x1,
+ m.x2,
+ m.T,
+ m.C,
+ m.consume_scrut
+ )
+ );
+ }
+
+ for (int i = 0; i < m.C.length; ++i) {
+ lift = liftSingleMatch(m.C[i].body);
+
+ if (lift != null) {
+ Case[] cases = (Case[])m.C.clone();
+ cases[i].body = lift.context;
+
+ return new LiftedMatch(
+ lift.scrut,
+ lift.hole,
+ lift.cases,
+ new Match(
+ m.t,
+ m.x1,
+ m.x2,
+ m.T,
+ cases,
+ m.consume_scrut
+ )
+ );
+ }
+
+ }
+
+ Var hole = new Var("hole");
+ return new LiftedMatch(
+ m.t,
+ hole,
+ m.C,
+ hole
+ );
+ case Expr.LET:
+ Let l = (Let)e;
+ lift = liftSingleMatch(l.t1);
+
+ if (lift != null) {
+ return new LiftedMatch(
+ lift.scrut,
+ lift.hole,
+ lift.cases,
+ new Let(
+ l.x1,
+ l.x1_stat,
+ lift.context,
+ l.x2,
+ l.t2
+ )
+ );
+ }
+
+ lift = liftSingleMatch(l.t2);
+
+ if (lift != null) {
+ return new LiftedMatch(
+ lift.scrut,
+ lift.hole,
+ lift.cases,
+ new Let(
+ l.x1,
+ l.x1_stat,
+ l.t1,
+ l.x2,
+ lift.context
+ )
+ );
+ }
+
+ return null;
+ default:
+ assert(false);
+ return null;
+ }
+ }
+
+ public boolean matchFree(Expr e)
+ {
+ switch(e.construct)
+ {
+ case Expr.TERM_APP:
+ TermApp ta = (TermApp)e;
+
+ boolean ret = true;
+
+ ret |= matchFree(ta.head);
+
+ for (int i = 0; i < ta.X.length; ++i)
+ ret |= matchFree(ta.X[i]);
+
+ return ret;
+ case Expr.FUN_TERM:
+
+ // We could lift matches from function bodies as well,
+ // but this wouldn't really reflect guru's
+ // call-by-value semantics.
+ return true;
+ case Expr.VAR:
+ return true;
+ case Expr.CONST:
+ return true;
+ case Expr.MATCH:
+ return false;
+ case Expr.LET:
+ Let let = (Let)e;
+ return matchFree(let.t1) && matchFree(let.t2);
+ default:
+ assert(false);
+ return false;
+ }
+ }
+
+ // Returns some variable used as a match inside expression e,
+ // or null if e contains no matches.
+// public Var UnAnnotatedTermTemplate(Expr e)
+// {
+// switch(e.construct)
+// {
+// case Expr.TERM_APP:
+// TermApp ta = (TermApp)e;
+// break;
+// case Expr.FUN_TERM:
+// FunTerm ft = (FunTerm)e;
+// break;
+// case Expr.VAR:
+// return null;
+// case Expr.CONST:
+// case Expr.MATCH:
+// Match m = (Match)e;
+// return m.t;
+// break;
+// case Expr.LET:
+// break;
+// default:
+// return null;
+// }
+// }
+
+ public Expr liftMatches(Expr e)
+ {
+ Vector lifts = new Vector();
+
+ LiftedMatch currentLift = liftSingleMatch(e);
+ while (currentLift != null)
+ {
+ lifts.add(currentLift);
+ currentLift = liftSingleMatch(currentLift.context);
+ }
+
+ if (lifts.size() == 0)
+ return e;
+ else
+ return liftsToExp(lifts,0);
+ }
+
+ public Expr liftsToExp(Vector lifts, int liftInd)
+ {
+ LiftedMatch lift = (LiftedMatch)lifts.get(liftInd);
+
+ Case[] cases = new Case[lift.cases.length];
+
+ for (int i = 0; i < lift.cases.length; ++i)
+ {
+ Case liftCase = lift.cases[i];
+
+ Expr body;
+
+
+ if (liftInd == lifts.size()-1) {
+ body = lift.context.subst(liftCase.body, lift.hole);
+ }
+ else {
+ body = liftsToExp(lifts, liftInd+1).subst(liftCase.body, lift.hole);
+ }
+
+ cases[i] = new Case(
+ liftCase.c,
+ liftCase.x,
+ body,
+ liftCase.impossible
+ );
+ }
+
+ Var junk = new Var("junk");
+
+ return new Match(
+ lift.scrut,
+ junk,
+ junk,
+ junk,
+ cases,
+ false
+ );
+ }
+
+ // An experimental version of instantiate using nueval
+ public Expr instantiate2(Context ctxt, Expr lhs)
+ {
+ if (lhs.construct != TERM_APP)
+ return lhs;
+
+ Expr lhs2 = lhs;
+
+ while (true) {
+ System.out.println("a.");
+ System.out.println(lhs2.toString(ctxt));
+
+ lhs2 = nueval(lhs2, ctxt);
+
+ System.out.println("b.");
+ System.out.println(lhs2.toString(ctxt));
+
+ lhs2 = liftMatches(lhs2);
+
+ System.out.println("c.");
+ System.out.println(lhs2.toString(ctxt));
+
+ if (lhs2.construct == TERM_APP)
+ {
+ TermApp ta = (TermApp)lhs2;
+
+ if (ta.head.construct != CONST)
+ return lhs2;
+
+ // The pre-instantiated value of the head.
+ Const c = (Const)ta.head;
+
+ // A variable used to instantiate the head
+ Expr ev = c.eval(ctxt);
+
+ if (ev.construct != FUN_TERM)
+ {
+ handleError(ctxt,
+ "The left hand side of an unjoin scrutinee " +
+ "evaluates to a term app whose head is not a function.\n" +
+ "1. lhs:" + lhs.toString(ctxt) + "\n" +
+ "2. evaluated lhs: " + ev.toString(ctxt) + "\n"
+ );
+ }
+
+ FunTerm inst = (FunTerm)ev;
+ Var r = inst.r;
+
+ // Apply all arguments except last.
+ for (int i = 0; i < ta.X.length-1; ++i)
+ inst = (FunTerm)inst.substituteForParam(ta.X[i]);
+
+ // Apply last argument.
+ // Instantiating a function with one argument may result in an
+ // arbitrary term, so we need to use an Expr rather than
+ // a FunTerm to hold the result.
+ lhs2 = inst.substituteForParam(ta.X[ta.X.length-1]);
+
+ // If we are unjoining an application of a recursive, top-level
+ // function, we substitute the function's constant for occurrences
+ // of the function's recursive variable in the body.
+ //
+ // This way, any facts deduced about recursive calls will mention
+ // the constant which, unlike the recursive variable, is accessible
+ // via the current context.
+ if (r != null)
+ lhs2= (Expr)lhs2.subst(c, r);
+ }
+ else
+ {
+ return lhs2;
+ }
+ }
+ }
+
+ // TODO: we need a base class for Unjoin and UnjoinContra which implements
+ // this.
+ //
+ // Converts the left hand side of the scrutinee atom into an equivalent
term
+ // from which unjoin can derive useful information. This equivalent term
+ // will either be a match, a let, or an abbrev.
+ //
+ // The conversion process is as follows:
+ //
+ // - While t is a term app:
+ // - if the head is a const defined to be some recursive function,
+ // establish a correspondence between the constant and the
function's
+ // recursive variable in the unjoin context
+ // - evaluate the head if possible
+ // - if the resulting head is a function term, instantiate the function
+ // in a lazy manner, substituting each actual argument for its
corresponding
+ // formal argument without evaluating the actuals.
+ // otherwise, generate an error and halt.
+ // - assign t to the instantiated function.
+ // - return t
+ //
+ // TODO: We might have to prove an equivalence between the strict function
+ // call semantics used by guru and the lazy approach taken by unjoin.
Since
+ // guru is functional, this should work.
+ private Expr instantiate(Context ctxt, Expr lhs)
+ {
+ if (lhs.construct != TERM_APP)
+ return lhs;
+
+ TermApp ta = (TermApp)lhs;
+
+ while (true) {
+ Expr h = ta.head.evalStep(ctxt);
+ //The constant or variable initially used for the head.
+ Expr pre = ta.head;
+
+ while (h != h.evalStep(ctxt));
+ {
+ if (h.construct == MATCH)
+ handleError(ctxt,
+ "Unjoin cannot handle terms containing term apps" +
+ " whose heads evaluate to matches.");
+
+ h = h.evalStep(ctxt);
+
+ }
+
+ //TODO: we really need to loop here, evaluating the head
+ //one step at a time until normalization, generating an
+ //error message if any intermediate form is not a constant.
+ //We only need to establish a correspondence between the
+ //initial const and the recursive variable of the normal form.
+
+ // If the head does not normalize to a function, we cannot
+ // instantiate it, so we cannot unjoin this term app.
+ if (h.construct != FUN_TERM) {
+ handleError(ctxt,
+ "The left hand side of an unjoin scrutinee " +
+ "evaluates to a term app whose head is not a function.\n" +
+ "1. lhs:" + lhs.toString(ctxt) + "\n" +
+ "2. evaluated lhs: " + h.toString(ctxt) + "\n"
+ );
+ }
+
+ // The pre-instantiated value of the head.
+ FunTerm f = (FunTerm)h;
+ // A variable used to instantiate the head
+ FunTerm inst = f;
+
+ // Apply all arguments except last.
+ for (int i = 0; i < ta.X.length-1; ++i)
+ inst = (FunTerm)inst.substituteForParam(ta.X[i]);
+
+ // Apply last argument.
+ // Instantiating a function with one argument may result in an
+ // arbitrary term, so we need to use an Expr rather than
+ // a FunTerm to hold the result.
+ Expr fullInstantiation = inst.substituteForParam(ta.X[ta.X.length-1]);
+
+ // If we are unjoining an application of a recursive, top-level
+ // function, we substitute the function's constant for occurrences
+ // of the function's recursive variable in the body.
+ //
+ // This way, any facts deduced about recursive calls will mention
+ // the constant which, unlike the recursive variable, is accessible
+ // via the current context.
+ if (f.r != null && pre.construct == CONST)
+ fullInstantiation = (Expr)fullInstantiation.subst((Const)pre, f.r);
+
+ //continue past lets and abbrevs
+ fullInstantiation = fullInstantiation.eval(ctxt);
+
+ if (fullInstantiation.construct != TERM_APP)
+ return fullInstantiation;
+
+ ta = (TermApp)fullInstantiation;
+ }
+ }
+
+ private void DumpUnjoinPaths(List unjoinPaths, Context ctxt)
+ {
+ for(int i = 0; i < unjoinPaths.size(); ++i) {
+ String pathString = "";
+ Stack path = (Stack)unjoinPaths.get(i);
+ for(int j = 0; j < path.size(); ++j) {
+ UnjoinIntro u = (UnjoinIntro)path.get(j);
+ pathString += "(" + u.introVar.toString(ctxt) + " : " +
+ u.introVarType.toString(ctxt) + ")";
+ }
+
+ System.out.println(pathString);
+ }
+ }
+
+ // Expr override
+ public Expr dropAnnos(Context ctxt) {
+ return new Bang();
+ }
+
+}
=======================================
--- /branches/1.0/guru/Const.java Thu Oct 27 08:11:15 2011
+++ /branches/1.0/guru/Const.java Mon Nov 14 12:52:03 2011
@@ -126,7 +126,7 @@
public UnjoinDeduction Unjoin(
Expr target,
- int proofCount,
+ UnjoinContext uctxt,
Context baseCtxt,
boolean eq
)
=======================================
--- /branches/1.0/guru/Expr.java Thu Oct 27 08:11:15 2011
+++ /branches/1.0/guru/Expr.java Mon Nov 14 12:52:03 2011
@@ -785,7 +785,7 @@
// target term.)
public UnjoinDeduction Unjoin(
Expr target,
- int proofCount,
+ UnjoinContext uctxt,
Context baseCtxt,
boolean eq
)
=======================================
--- /branches/1.0/guru/LemmaSet.java Mon Oct 31 13:11:32 2011
+++ /branches/1.0/guru/LemmaSet.java Mon Nov 14 12:52:03 2011
@@ -90,9 +90,15 @@
{
e_ = e;
- if (e.construct == Expr.TERM_APP)
- break;
-
+ if (e.construct == Expr.TERM_APP) {
+ TermApp ta = (TermApp)e;
+
+ if (ta.head.construct == Expr.CONST) {
+ Const c = (Const)ta.head;
+ if (ctxt.isTermCtor(c))
+ break;
+ }
+ }
if (e.construct == Expr.MATCH) {
Match m = (Match)e;
Expr mt_ = simplify(m.t);
@@ -108,8 +114,8 @@
}
}
- e = e.evalStep(ctxt);
e = rewrite(e);
+ e = e.evalStep(ctxt);
}
return e;
@@ -158,13 +164,8 @@
return ret;
}
- private Expr rewrite(Expr e)
- {
- if (e.construct != Expr.VAR)
- return e;
-
- Var v = (Var)e;
-
+ public Expr rewrite(Expr e)
+ {
ListIterator i = formulas.listIterator();
while(i.hasNext()) {
Expr curr = (Expr)i.next();
@@ -177,7 +178,7 @@
if (a.equality == false)
continue;
- if (a.Y1 == v) {
+ if (a.Y1.defEq(ctxt, e)) {
if (a.Y2.construct == Expr.TERM_APP)
{
TermApp ta = (TermApp)a.Y2;
@@ -191,7 +192,7 @@
}
}
- if (a.Y2 == v && a.Y1.construct == Expr.TERM_APP) {
+ if (a.Y2.defEq(ctxt, e) && a.Y1.construct == Expr.TERM_APP) {
if (a.Y1.construct == Expr.TERM_APP)
{
TermApp ta = (TermApp)a.Y1;
@@ -206,6 +207,6 @@
}
}
- return v;
+ return e;
}
}
=======================================
--- /branches/1.0/guru/Let.java Mon Oct 31 13:11:32 2011
+++ /branches/1.0/guru/Let.java Mon Nov 14 12:52:03 2011
@@ -169,14 +169,14 @@
// Overloaded from Expr
public UnjoinDeduction Unjoin(
Expr target,
- int proofCount,
+ UnjoinContext uctxt,
Context ctxt,
boolean eq
)
{
return t2.subst(t1, x1).Unjoin(
target,
- proofCount,
+ uctxt,
ctxt,
eq
);
=======================================
--- /branches/1.0/guru/Match.java Mon Oct 31 13:11:32 2011
+++ /branches/1.0/guru/Match.java Mon Nov 14 12:52:03 2011
@@ -162,14 +162,14 @@
//Override from Expr
public UnjoinDeduction Unjoin(
Expr target,
- int proofCount,
+ UnjoinContext uctxt,
Context baseCtxt,
boolean eq
)
{
UnjoinDeduction ret = UnjoinDeduction.contradiction;
- Expr t_ = baseCtxt.lemmaSet.simplify(t);
+ Expr t_ = uctxt.lemmaSet.rewrite(t);
//baseCtxt.lemmaSet.instantiate(t);
//while (t_.construct != TERM_APP && t_ != t_.evalStep(baseCtxt))
@@ -184,8 +184,14 @@
Case c = C[i];
//TODO: do we really have to do this to detect term constructors?
- boolean isTermConstructor = t_.construct == TERM_APP &&
t_.evalStep(baseCtxt) == t_;
- if (isTermConstructor) {
+ boolean isConstructorTerm = t_.construct == TERM_APP;
+ if (isConstructorTerm)
+ isConstructorTerm &= ((TermApp)t_).head.construct == Expr.CONST;
+
+ if (isConstructorTerm)
+ isConstructorTerm &= baseCtxt.isTermCtor( (Const)((TermApp)t_).head
);
+
+ if (isConstructorTerm) {
if (((TermApp)t_).head != c.c)
continue;
}
@@ -196,27 +202,37 @@
// Prepend immediate deductions onto case body deductions -----
if (c.x.length == 0) {
+
+ Atom matchEq = new Atom(true, t_, c.c);
+ Var matchEqVar = new Var("p" + uctxt.proofCounter);
+
+ if (t_.construct != CONST)
+ {
+ uctxt.proofCounter++;
+ uctxt.lemmaSet.addLemma(matchEq);
+ }
+
// Make deductions from case body -----
branch = c.body.Unjoin(
target,
- t_.construct == CONST ? proofCount : proofCount + 1,
+ uctxt,
baseCtxt,
eq
);
if (t_.construct != CONST) {
- Atom matchEq = new Atom(true, t_, c.c);
- Var matchEqVar = new Var("p" + proofCount);
+ uctxt.proofCounter--;
+ uctxt.lemmaSet.removeLemma(matchEq);
+
branch = new UnjoinIntro(matchEqVar, matchEq, branch);
}
}
else {
- FunType consType =
(FunType)c.c.classify(baseCtxt).defExpandTop(baseCtxt);
-
+
Expr body = c.body;
// Create argument variables -----
- if (t_.construct == TERM_APP) {
+ if (isConstructorTerm) {
TermApp ta = (TermApp)t_;
for (int j = 0; j < ta.X.length; ++j)
@@ -224,43 +240,79 @@
branch = body.Unjoin(
target,
- proofCount,
+ uctxt,
baseCtxt,
eq
);
}
else {
- Var[] clones = new Var[c.x.length];
- Expr[] types = new Expr[c.x.length];
- int last = c.x.length-1;
-
- for(int j = 0; j <= last; ++j)
- {
- clones[j] = new Var(((Var)t_).name + j);
- types[j] = consType.types[j];
-
- body = body.subst(clones[j], c.x[j]);
+ FunType consType =
(FunType)c.c.classify(baseCtxt).defExpandTop(baseCtxt);
+
+ Var[] clones = new Var[consType.vars.length];
+ Var[] nonSpecificationalClones = new Var[c.x.length];
+ Expr[] types = new Expr[consType.vars.length];
+ int last = consType.vars.length-1;
+
+ //index into non-specificational args
+ int uInd = 0;
+
+ for(int j = 0; j < clones.length; ++j)
+ {
+ String name;
+ if (t_.construct == VAR)
+ name = ((Var)t_).name + j;
+ else
+ name = "c" + j;
+
+ clones[j] = new Var(name);
+ types[j] = consType.types[0];
+ baseCtxt.setClassifier(clones[j], types[j]);
+
+ int spec = (consType.owned[0].status & Ownership.SPEC);
+
+ if (!(clones[j].isTypeOrKind(baseCtxt) ||
+ clones[j].isProof(baseCtxt) ||
+ spec != 0) ) {
+
+ nonSpecificationalClones[uInd] = clones[j];
+ body = body.subst(clones[j], c.x[uInd]);
+ uInd++;
+ }
// Instantiating the last argument would result in the
// return type, which may not be a function type.
if (j != last)
consType = (FunType)consType.instantiate(clones[j]);
}
+
+
+ Atom matchEq = new Atom(
+ true,
+ t_,
+ new TermApp(c.c,nonSpecificationalClones)
+ );
+
+ Var matchEqVar = new Var("p" + uctxt.proofCounter);
+ baseCtxt.setClassifier(matchEqVar, matchEq);
+
+ uctxt.proofCounter++;
+ uctxt.lemmaSet.addLemma(matchEq);
// Make deductions from case body -----
branch = body.Unjoin(
target,
- proofCount+1,
+ uctxt,
baseCtxt,
eq
);
+
+ uctxt.proofCounter--;
+ uctxt.lemmaSet.removeLemma(matchEq);
//prepend immediate deductions to case body deductions
- Atom matchEq = new Atom(true, t_, new TermApp(c.c,clones));
- Var matchEqVar = new Var("p" + proofCount);
branch = new UnjoinIntro(matchEqVar, matchEq, branch);
- for (int j = c.x.length-1; j >= 0; --j)
+ for (int j = types.length-1; j >= 0; --j)
branch = new UnjoinIntro(clones[j], types[j], branch);
}
}
=======================================
--- /branches/1.0/guru/TermApp.java Mon Oct 31 13:11:32 2011
+++ /branches/1.0/guru/TermApp.java Mon Nov 14 12:52:03 2011
@@ -516,7 +516,7 @@
public UnjoinDeduction Unjoin(
Expr target,
- int proofCount,
+ UnjoinContext uctxt,
Context baseCtxt,
boolean eq
)
=======================================
--- /branches/1.0/guru/Unjoin.java Mon Oct 31 13:11:32 2011
+++ /branches/1.0/guru/Unjoin.java Mon Nov 14 12:52:03 2011
@@ -91,23 +91,20 @@
* is needed for this, which is implemented in UnjoinContra.java.
*
*/
-public class Unjoin extends Expr {
-
- // An expression which proves the scrutinee atom.
- public final Expr scrutineeProof;
-
- // A list containing forall proofs which quantify over the
- // deductions made in each unjoin path.
+public class Unjoin extends UnjoinBase {
+
+ /** A list containing forall proofs which quantify over the
+ * deductions made in each unjoin path.
+ */
public final Vector paths;
public Unjoin(Expr scrutineeProof, Vector paths)
{
- super(UNJOIN);
+ super(UNJOIN, scrutineeProof);
assert(scrutineeProof != null);
assert(paths != null);
- this.scrutineeProof = scrutineeProof;
this.paths = paths;
}
@@ -122,117 +119,6 @@
}
w.print("end");
}
-
- public static boolean placeHolder(Expr e, Context ctxt)
- {
- if (e.construct == VAR)
- return true;
-
- if (e.construct == CONST && e.evalStep(ctxt) != e)
- return true;
-
- return false;
- }
-
- // TODO: we need a base class for Unjoin and UnjoinContra which implements
- // this.
- //
- // Converts the left hand side of the scrutinee atom into an equivalent
term
- // from which unjoin can derive useful information. This equivalent term
- // will either be a match, a let, or an abbrev.
- //
- // The conversion process is as follows:
- //
- // - While t is a term app:
- // - if the head is a const defined to be some recursive function,
- // establish a correspondence between the constant and the
function's
- // recursive variable in the unjoin context
- // - evaluate the head if possible
- // - if the resulting head is a function term, instantiate the function
- // in a lazy manner, substituting each actual argument for its
corresponding
- // formal argument without evaluating the actuals.
- // otherwise, generate an error and halt.
- // - assign t to the instantiated function.
- // - return t
- //
- // TODO: We might have to prove an equivalence between the strict function
- // call semantics used by guru and the lazy approach taken by unjoin.
Since
- // guru is functional, this should work.
- private Expr instantiate(Context ctxt, Expr lhs)
- {
- if (lhs.construct != TERM_APP)
- return lhs;
-
- TermApp ta = (TermApp)lhs;
-
- while (true) {
- Expr h = ta.head.evalStep(ctxt);
- //The constant or variable initially used for the head.
- Expr pre = ta.head;
-
- while (h != h.evalStep(ctxt));
- {
- if (h.construct == MATCH)
- handleError(ctxt,
- "Unjoin cannot handle terms containing term apps" +
- " whose heads evaluate to matches.");
-
- h = h.evalStep(ctxt);
-
- }
-
-
- //TODO: we really need to loop here, evaluating the head
- //one step at a time until normalization, generating an
- //error message if any intermediate form is not a constant.
- //We only need to establish a correspondence between the
- //initial const and the recursive variable of the normal form.
-
- // If the head does not normalize to a function, we cannot
- // instantiate it, so we cannot unjoin this term app.
- if (h.construct != FUN_TERM) {
- handleError(ctxt,
- "The left hand side of an unjoin scrutinee " +
- "evaluates to a term app whose head is not a function.\n" +
- "1. lhs:" + lhs.toString(ctxt) + "\n" +
- "2. evaluated lhs: " + h.toString(ctxt) + "\n"
- );
- }
-
- // The pre-instantiated value of the head.
- FunTerm f = (FunTerm)h;
- // A variable used to instantiate the head
- FunTerm inst = f;
-
- // Apply all arguments except last.
- for (int i = 0; i < ta.X.length-1; ++i)
- inst = (FunTerm)inst.substituteForParam(ta.X[i]);
-
- // Apply last argument.
- // Instantiating a function with one argument may result in an
- // arbitrary term, so we need to use an Expr rather than
- // a FunTerm to hold the result.
- Expr fullInstantiation = inst.substituteForParam(ta.X[ta.X.length-1]);
-
- // If we are unjoining an application of a recursive, top-level
- // function, we substitute the function's constant for occurrences
- // of the function's recursive variable in the body.
- //
- // This way, any facts deduced about recursive calls will mention
- // the constant which, unlike the recursive variable, is accessible
- // via the current context.
- if (f.r != null && pre.construct == CONST)
- fullInstantiation = (Expr)fullInstantiation.subst((Const)pre, f.r);
-
- //continue past lets and abbrevs
- fullInstantiation = fullInstantiation.eval(ctxt);
-
- if (fullInstantiation.construct != TERM_APP)
- return fullInstantiation;
-
- ta = (TermApp)fullInstantiation;
- }
- }
// Checks that each parsed path (a forall proof) can eliminate the
// corresponding unjoined path (and exists proof), and that every such
@@ -305,11 +191,12 @@
}
- Expr instantiated = instantiate(ctxt, scrutinee.Y1);
+ Expr instantiated = instantiate2(ctxt, scrutinee.Y1);
+ UnjoinContext uctxt = new UnjoinContext(ctxt.lemmaSet);
UnjoinDeduction deduction = instantiated.Unjoin(
scrutinee.Y2,
- 0,
+ uctxt,
ctxt,
scrutinee.equality
);
=======================================
--- /branches/1.0/guru/UnjoinContext.java Thu Oct 27 08:11:15 2011
+++ /branches/1.0/guru/UnjoinContext.java Mon Nov 14 12:52:03 2011
@@ -18,11 +18,11 @@
// unique.
public int proofCounter;
- // The recursive variable of the function being unjoined.
- // If this is null, then we are not unjoining an application of a
recursive,
- // top-level function, or it hasn't been set yet.
- public Var recVar;
-
- // The constant representing the function being unjoined.
- public Const recConst;
-}
+ public final LemmaSet lemmaSet;
+
+ public UnjoinContext(LemmaSet baseLemmaSet)
+ {
+ this.proofCounter = 0;
+ this.lemmaSet = baseLemmaSet.copy();
+ }
+}
=======================================
--- /branches/1.0/guru/UnjoinContra.java Thu Oct 27 08:11:15 2011
+++ /branches/1.0/guru/UnjoinContra.java Mon Nov 14 12:52:03 2011
@@ -41,10 +41,7 @@
* UnjoinContra's implementation is very similar to Unjoin's. See
* Unjoin.java for a more detailed explanation of how unjoining works.
*/
-public class UnjoinContra extends Expr {
-
- // An expression which proves the scrutinee atom.
- public final Expr scrutineeProof;
+public class UnjoinContra extends UnjoinBase {
// The formula, written by the programmer, which the contradiction
// is being used to prove.
@@ -52,12 +49,11 @@
public UnjoinContra(Expr scrutineeProof, Expr conclusion)
{
- super(UNJOIN_CONTRA);
+ super(UNJOIN_CONTRA, scrutineeProof);
assert(scrutineeProof != null);
assert(conclusion != null);
- this.scrutineeProof = scrutineeProof;
this.conclusion = conclusion;
}
@@ -76,87 +72,6 @@
System.out.println(pathString);
}
}
-
- // Converts the left hand side of the scrutinee atom into an equivalent
term
- // from which unjoin can derive useful information. This equivalent term
- // will either be a match, a let, or an abbrev.
- //
- // The conversion process is as follows:
- //
- // - While t is a term app:
- // - if the head is a const defined to be some recursive function,
- // establish a correspondence between the constant and the
function's
- // recursive variable in the unjoin context
- // - evaluate the head if possible
- // - if the resulting head is a function term, instantiate the function
- // in a lazy manner, substituting each actual argument for its
corresponding
- // formal argument without evaluating the actuals.
- // otherwise, generate an error and halt.
- // - assign t to the instantiated function.
- // - return t
- private Expr instantiate(Context ctxt, Expr lhs)
- {
- if (lhs.construct != TERM_APP)
- return lhs;
-
- TermApp ta = (TermApp)lhs;
-
- while (true) {
- //The head, normalized to a function term
- Expr h = ta.head.evalStep(ctxt);
- //The constant or variable initially used for the head.
- Expr pre = ta.head;
-
- //TODO: we really need to loop here, evaluating the head
- //one step at a time until normalization, generating an
- //error message if any intermediate form is not a constant.
- //We only need to establish a correspondence between the
- //initial const and the recursive variable of the normal form.
-
- // If the head does not normalize to a function, we cannot
- // instantiate it, so we cannot unjoin this term app.
- if (h.construct != FUN_TERM) {
- handleError(ctxt,
- "The left hand side of an unjoin scrutinee " +
- "simplifies to a term app whose head is not a function.\n" +
- "1. lhs:" + lhs.toString(ctxt) + "\n" +
- "2. simplified lhs: " + h.toString(ctxt) + "\n"
- );
- }
-
- // The pre-instantiated value of the head.
- FunTerm f = (FunTerm)h;
- // A variable used to instantiate the head
- FunTerm inst = f;
-
- // Apply all arguments except last.
- for (int i = 0; i < ta.X.length-1; ++i)
- inst = (FunTerm)inst.substituteForParam(ta.X[i]);
-
- // Apply last argument.
- // Instantiating a function with one argument may result in an
- // arbitrary term, so we need to use an Expr rather than
- // a FunTerm to hold the result.
- Expr fullInstantiation = inst.substituteForParam(ta.X[ta.X.length-1]);
-
- // If we are unjoining an application of a recursive, top-level
- // function, we substitute the function's constant for occurrences
- // of the function's recursive variable in the body.
- //
- // This way, any facts deduced about recursive calls will mention
- // the constant which, unlike the recursive variable, is accessible
- // via the current context.
- if (f.r != null && pre.construct == CONST)
- fullInstantiation = (Expr)fullInstantiation.subst((Const)pre, f.r);
-
- //TODO: substitute lets and abbrevs here?
-
- if (fullInstantiation.construct != TERM_APP)
- return fullInstantiation;
-
- ta = (TermApp)fullInstantiation;
- }
- }
public Expr classify(Context ctxt) {
Expr cScrutProof = scrutineeProof.classify(ctxt);
@@ -183,12 +98,13 @@
System.exit(0);
}
- Expr instantiated = instantiate(ctxt, scrutinee.Y1);
- instantiated = ctxt.lemmaSet.instantiate(instantiated);
+ Expr instantiated = instantiate2(ctxt, scrutinee.Y1);
+ instantiated = ctxt.lemmaSet.rewrite(instantiated);
+ UnjoinContext uctxt = new UnjoinContext(ctxt.lemmaSet);
UnjoinDeduction deduction = instantiated.Unjoin(
scrutinee.Y2,
- 0,
+ uctxt,
ctxt,
scrutinee.equality
);
=======================================
--- /branches/1.0/guru/Var.java Mon Oct 31 13:11:32 2011
+++ /branches/1.0/guru/Var.java Mon Nov 14 12:52:03 2011
@@ -158,7 +158,7 @@
public UnjoinDeduction Unjoin(
Expr target,
- int proofCount,
+ UnjoinContext uctxt,
Context baseCtxt,
boolean eq
)
@@ -166,7 +166,7 @@
if (baseCtxt.isMacroDefined(this)) {
//TODO: this should be removed... abbrevs should be substituted
//before unjoining.
- return evalStep(baseCtxt).Unjoin(target, proofCount, baseCtxt, eq);
+ return evalStep(baseCtxt).Unjoin(target, uctxt, baseCtxt, eq);
}
else {
if (target == this)
=======================================
--- /branches/1.0/tests/unjoin.g Mon Oct 31 13:11:32 2011
+++ /branches/1.0/tests/unjoin.g Mon Nov 14 12:52:03 2011
@@ -5,6 +5,82 @@
Include "../lib/vec.g"
Include "../lib/minmax.g"
+
+Inductive list2 : Fun(A:type).type :=
+ | nil2 : Fun(A:type).<list2 A>
+ | cons2 : Fun(A:type)(a:A)(l:<list2 A>). <list2 A>.
+
+Define foldr2
+ : Fun(S A : type)(acc : Fun(s : S)(a : A). S)(init : S)(l : <list2 A>). S
+:=
+ fun foldr2(S A : type)(acc : Fun(s : S)(a : A). S)(s : S)(l : <list2
A>):S.
+ match l with
+ | nil2 _ =>
+ s
+ | cons2 _ a' l' =>
+ let s' = (acc s a') in
+ (foldr2 S A acc s' l')
+ end.
+
+Define ormap :=
+ fun(l : <list2 bool>).
+ (foldr2 bool bool or ff l).
+%-
+Define list_setmember2
+ : Forall(A:type)(a:A)
+ (eqA:Fun(^#owned x y: A).bool)
+ (eqA_total:Forall(a b: A).Exists(z:bool).{ (eqA a b) = z })
+ (u:{ (eqA a a) = tt })
+ (l'' l':<list A>).
+ { (member a (append l' (cons a l'')) eqA) = tt }
+:=
+ foralli(A:type)(a:A)(eqA:Fun(^ #owned x y: A).bool)
+ (eqA_total:Forall(a b: A).Exists(z:bool).{ (eqA a b) = z })
+ (u: {(eqA a a) = tt})(l'' l':<list A>).
+ abbrev eqA = terminates eqA by eqA_total in
+ case (member A a (append A l' (cons A a l'')) eqA) by v ign with
+ | ff =>
+ lemma u in
+ unjoin v with
+ | foralli(p0 : { (append l' (cons a l'')) = nil }).
+ unjoin p0 with
+
+ | (l'0 : type)(l'1 : l'0)(l'2 : <list l'0>)(p0 : { l' = (cons l'1
l'2) })
+ (u : { (append_h (inspect mk_append_i) l'1 (foldr (clone_owned
(inspect mk_append_i)) append_h (cons a l'') l'2)) = nil }) =>
+
+
+ %-
+ %%
+ %% INTERESTING POINT - PARTIAL APPLICATION USED TO CREATE A FUNCTION
+ %% DOES NOT HANDLE WELL. NUEVAL
+ %%
+ %%
+ | foralli(l'0 : type)(l'1 : l'0)(l'2 : <list l'0>)
+ (p0 : { l' = (cons l'1 l'2) })
+ (u : { (fun(^ #owned cookie)(^ #owned x)(l) : !. match
cookie by cookie_eq cookie_Eq return <list A> with mk_append_i => (cons
(inc_owned x) l) end mk_append_i l'1 (fun foldr(^ #owned cookie)(fcn)(b)(^
#owned l) : !. match l by l_eq l_Eq return B with nil => b | cons a' l' =>
(fcn cookie a' (foldr (clone_owned cookie) fcn b l')) end (clone_owned
mk_append_i) fun(^ #owned cookie)(^ #owned x)(l) : !. match cookie by
cookie_eq cookie_Eq return <list A> with mk_append_i => (cons (inc_owned x)
l) end (cons a l'') l'2)) = nil })
+ -%
+
+ end
+
+ | foralli(c0 : type)(c1 : c0)(c2 : <list c0>)
+ (p0 : { (append l' (cons a l'')) = (cons c1 c2) })
+ (u : { (or (eqA (clone_owned a) c1) (member a c2 eqA)) = ff
}).
+ truei
+ end
+
+ | tt =>
+ v
+ end
+-%
+
+
+Define eqnatEq3 : Forall(n:nat)(u:{(eqnat n Z) = tt}). { n = Z } :=
+ foralli(n: nat)(u:{(eqnat n Z) = tt}).
+ unjoin u with
+ | foralli(p4 : { n = Z }).
+ p4
+ end.
+
Define letFunc :=
fun (x : bool).
let x = (or x x) in
@@ -103,16 +179,6 @@
u
end.
-Define max2 : Fun(a b:nat).nat :=
- fun max(a b :nat) : nat.
- match a by u u return nat with
- Z => b
- | S a' => match b by u u return nat with
- Z => a
- | S b' => (S (max a' b'))
- end
- end.
-
Define matchArgs :=
fun(x : nat)(y : nat).
let z =
@@ -123,13 +189,28 @@
two
end
in
- (max2 z y).
+ (max z y).
Define matchArgsProof
-
:=
foralli(x y : nat)(u : { (matchArgs x y) = two }).
unjoin u with
+ | foralli(p0 : { x = Z })(u : { (max one y) = two }).
+ lemma
+ : { (le y (max one y)) = tt }
+ [max_easy y one]
+ : { (le (max one y) two) = tt }
+ [eq_le (max one y) two u]
+ in
+ [le_trans y (max one y) two ## ##]
+ | foralli(x0 : nat)(p0 : { x = (S x0) })(u : { (max two y) = two }).
+ lemma
+ : { (le y (max two y)) = tt }
+ [max_easy y two]
+ : { (le (max two y) two) = tt }
+ [eq_le (max two y) two u]
+ in
+ [le_trans y (max two y) two ## ##]
end.
@@ -165,106 +246,14 @@
end
end
end.
-
+
+
+
%
% MOAR PROOOFS
%
%
-%-
-Define myproof :=
- foralli(a b : nat)(x:{ (lt a b) = tt } ).
- unjoin x with
- | foralli(p2 : { a = Z })(b' : nat)(p1 : { b = (S b') }).
- trans : { b = (S b') } p1
- : { (S b') != Z } clash (S b') Z
- | foralli(a' : nat)(p5 : { a = (S a') })(b' : nat)(p4 : { b = (S b') })
- (u : { (lt a' b') = tt }).
- trans : { b = (S b') } p4
- : { (S b') != Z } clash (S b') Z
- end.
--%
-
-Define eqnat : Fun(n m:nat).bool :=
- fun eqnat(n m:nat):bool.
- match n with
- | Z =>
- match m with
- | Z => tt
- | S m' => ff
- end
- | S n' =>
- match m with
- | Z => ff
- | S m' => (eqnat n' m')
- end
- end
- end.
-
-Define eqnatEq2 : Forall(n m:nat)(u:{(eqnat n m) = tt}). { n = m } :=
- induction(n:nat) return
- Forall(m:nat)(u:{(eqnat n m) = tt}). { n = m }
- with
- | Z =>
- foralli(m: nat)(u : { (eqnat n m) = tt }).
- case m with
- | Z =>
- transs
- : { m = Z } m_eq
- : { Z = n } symm n_eq
- end
- | S m' =>
- lemma
- : { (eqnat n m) = ff }
- hypjoin (eqnat n m) ff by
- : { m = (S m') } m_eq
- : { n = Z } n_eq
- end
- : { tt = ff }
- transs
- : { tt = (eqnat n m) } symm u
- : { (eqnat n m) = ff } ##
- end
- in
- contra
- : { tt = ff } ##
- { n = m }
- end
- | S n' =>
- foralli(m: nat)(u : { (eqnat n m) = tt }).
- case m with
- | Z =>
- lemma
- : { (eqnat n m) = ff }
- hypjoin (eqnat n m) ff by
- : { n = (S n') } n_eq
- : { m = Z } m_eq
- end
- : { tt = ff }
- transs
- : { tt = (eqnat n m) } symm u
- : { (eqnat n m) = ff } ##
- end
- in
- contra
- : { tt = ff } ##
- { n = m }
- | S m' =>
- hypjoin n m by
- : { n' = m' } [n_IH n' m' u]
- : { m = (S m') } m_eq
- : { n = (S n') } n_eq
- end
- end
- end.
-
-Define eqnatEq3 : Forall(n:nat)(u:{(eqnat n Z) = tt}). { n = Z } :=
- foralli(n: nat)(u:{(eqnat n Z) = tt}).
- unjoin u with
- | foralli(p4 : { n = Z }).
- p4
- end.
-
Define eqnatNeq2 : Forall(n m:nat)(u:{(eqnat n m) = ff}). { n != m } :=
induction (n:nat) return
Forall(m:nat)(u:{(eqnat n m) = ff}). { n != m }
@@ -366,21 +355,6 @@
end.
- %-
-Define lt_leff : Forall(a b:nat)(u:{ (lt a b) = tt }).{ (le b a) = ff }
- :=
- induction(a b: nat) return
- return Forall(u:{ (lt a b) = tt }).{ (le b a) = ff }
- with
- | Z =>
- foralli(u:{ (lt a b) = tt }).
- unjoin u with
- | contradiction.
- end
- | S n' =>
- end
--%
-
%- Define lt_ltff -- a lot like lt_leff -%
%-
@@ -559,111 +533,4 @@
end.
-%
-
- %-
-Define vec_last_eq_get_pred_n :
- Forall(A: type)
- (n: nat)
- (m: nat)
- (u: { (S m) = n })
- (v: <vec A n>)
- .
- { (vec_get v m) = (vec_last v) }
- :=
- foralli(A: type).
- induction(n: nat)
- return
- Forall(m: nat)(u: { (S m) = n })(v: <vec A n>). { (vec_get v m) =
(vec_last v) }
- with
- | Z =>
- foralli(m: nat)(u: { (S m) = n })(v: <vec A n>).
- contra
- transs
- symm n_eq %{ (Z = n) }
- symm u
- clash (S m) Z
- end
-
- { (vec_get v m) = (vec_last v) }
- | S n' =>
- foralli(m: nat)(u: { (S m) = n })(v: <vec A n>).
- abbrev Sn'_eq_Sm =
- trans u
- n_eq
- in
- abbrev m_eq_n' = inj (S *) Sn'_eq_Sm in
- case v with
- | vecn _ =>
- contra
- transs
- symm n_eq
- inj <vec ** *> v_Eq
- clash Z (S n')
- end
-
- { (vec_get v m) = (vec_last v) }
- | vecc _ restLen a rest =>
- abbrev SrestLen_eq_Sn' =
- trans inj <vec ** *> symm v_Eq %(S restLen) = n
- n_eq
- in
- abbrev restLen_eq_n' = inj (S *) SrestLen_eq_Sn' in
-
- case m with
- | Z =>
- case rest with
- | vecn _ =>
- hypjoin (vec_get v m) (vec_last v) by v_eq m_eq rest_eq
end
- | vecc _ x _ _ =>
- contra
- transs
- symm m_eq
- m_eq_n'
- symm restLen_eq_n'
- inj <vec ** *> rest_Eq %<vec A restLen> = <vec A (S
x)>
- clash (S x) Z
- end
-
- { (vec_get v m) = (vec_last v) }
- end
- | S m' =>
- abbrev Sm'_eq_n' = hypjoin (S m') n' by m_eq_n' m_eq n_eq
end in
- abbrev Sm'_le_n' = [eq_le (S m') n' Sm'_eq_n'] in
- abbrev m'_lt_Sm' = [lt_S m'] in
- abbrev m'_lt_n' = [ltle_trans m' (S m') n' m'_lt_Sm'
Sm'_le_n'] in
- % (vec_get rest m') = (vec_last rest)
- abbrev indStep =
- [n_IH
- n'
- m'
- Sm'_eq_n'
- cast rest by cong <vec A *> restLen_eq_n'
- ]
- in
- abbrev n'_neq_Z =
- trans symm Sm'_eq_n'
- clash (S m') Z
- in
- % { (vec_last rest) = (vec_last (vecc a rest)) }
- abbrev last_rest_eq_last_v =
- [vec_vecc_last_invariant
- A
- n'
- n'_neq_Z
- cast rest by cong <vec A *> restLen_eq_n'
- a
- ]
- in
- hypjoin (vec_get v m) (vec_last v) by
- indStep
- last_rest_eq_last_v
- v_eq
- m_eq
- end
- end
- end
- end.
-
--%
-
Classify eqnatNeq2.