[guru-lang] r549 committed - Added broken type reconstruction, with the intent of fixing it or comp...
guru...@googlecode.com
Author: kevinclancy0
Date: Mon Nov 28 13:07:03 2011
Log: Added broken type reconstruction, with the intent of fixing it or
completely reworking it at some point. Also added some more tests.
http://code.google.com/p/guru-lang/source/detail?r=549
Modified:
/branches/1.0/guru/Abbrev.java
/branches/1.0/guru/Expr.java
/branches/1.0/guru/LemmaSet.java
/branches/1.0/guru/Match.java
/branches/1.0/guru/UnjoinBase.java
/branches/1.0/tests/unjoin.g
=======================================
--- /branches/1.0/guru/Abbrev.java Mon Aug 22 15:38:29 2011
+++ /branches/1.0/guru/Abbrev.java Mon Nov 28 13:07:03 2011
@@ -134,6 +134,16 @@
return s;
}
+ public UnjoinDeduction Unjoin(
+ Expr target,
+ UnjoinContext uctxt,
+ Context baseCtxt,
+ boolean eq
+ )
+ {
+ return evalStep(baseCtxt).Unjoin(target, uctxt, baseCtxt, eq);
+ }
+
public Expr do_rewrite(Context ctxt, Expr e, Expr x, Stack boundVars) {
return subst().do_rewrite(ctxt, e, x, boundVars);
=======================================
--- /branches/1.0/guru/Expr.java Mon Nov 14 12:52:03 2011
+++ /branches/1.0/guru/Expr.java Mon Nov 28 13:07:03 2011
@@ -1,7 +1,9 @@
package guru;
-import java.util.*;
-import java.io.*;
+import java.util.Collection;
+import java.util.Enumeration;
+import java.util.Stack;
+import java.util.TreeSet;
public abstract class Expr {
=======================================
--- /branches/1.0/guru/LemmaSet.java Mon Nov 14 12:52:03 2011
+++ /branches/1.0/guru/LemmaSet.java Mon Nov 28 13:07:03 2011
@@ -1,212 +1,226 @@
package guru;
import java.util.ArrayList;
+import java.util.HashMap;
import java.util.ListIterator;
/**
* A set of all unnamed formulas which have been established in the current
- * context. Unnamed formulas can be used as premises for proof
instantiation
- * by using the ## token. They are introduced to the context using the
lemma
- * construct (see Lemma.java).
- *
+ * context. Unnamed formulas can be used as premises for proof
instantiation by
+ * using the ## token. They are introduced to the context using the lemma
+ * construct (see Lemma.java).
+ *
* NOTE: The java API's set classes are not suitable for defining a lemma
set
* due to their usage of the equals method to determine uniqueness. The
equals
- * method is not parameterized by context whereas our notion of
definitional equality is.
-*/
+ * method is not parameterized by context whereas our notion of
definitional
+ * equality is.
+ */
public class LemmaSet {
/** The context used to decide definitional equality */
final private Context ctxt;
-
- /** The set of definitionally unique formulas currently
- * contained in this lemma set.
+
+ /**
+ * The set of definitionally unique formulas currently contained in this
+ * lemma set.
*/
- final private ArrayList formulas;
-
- public LemmaSet(Context ctxt)
- {
- assert(ctxt != null);
-
+ final private ArrayList formulas;
+
+ public LemmaSet(Context ctxt) {
+ assert (ctxt != null);
+
this.ctxt = ctxt;
this.formulas = new ArrayList();
}
-
- /** Adds a lemma to the set. This lemma must be definitionally unequal
- * to each lemma currently in the set. (Use the HasLemma method to
- * determine whether or not an equivalent lemma is already in the set.)
- */
- public void addLemma(Expr newLemma)
- {
- assert(newLemma.isFormula(ctxt));
- assert(!hasLemma(newLemma));
-
+
+ /**
+ * Adds a lemma to the set. This lemma must be definitionally unequal to
+ * each lemma currently in the set. (Use the HasLemma method to determine
+ * whether or not an equivalent lemma is already in the set.)
+ */
+ public void addLemma(Expr newLemma) {
+ assert (newLemma.isFormula(ctxt));
+ assert (!hasLemma(newLemma));
+
formulas.add(newLemma);
}
-
+
/** Removes a lemma from the set. */
- public void removeLemma(Expr toRemove)
- {
- assert(toRemove.isFormula(ctxt));
- assert(hasLemma(toRemove));
-
+ public void removeLemma(Expr toRemove) {
+ assert (toRemove.isFormula(ctxt));
+ assert (hasLemma(toRemove));
+
formulas.remove(toRemove);
}
-
+
/** Returns true iff the given lemma is contained in this set */
- public boolean hasLemma(Expr lemma)
- {
- assert(lemma.isFormula(ctxt));
-
+ public boolean hasLemma(Expr lemma) {
+ assert (lemma.isFormula(ctxt));
+
ListIterator i = formulas.listIterator();
- while(i.hasNext())
- {
- Expr curr = (Expr)i.next();
-
+ while (i.hasNext()) {
+ Expr curr = (Expr) i.next();
+
if (curr.defEq(ctxt, lemma))
return true;
}
return false;
}
-
- /** Returns a new lemma set containing exactly the same set of formulas as
- * this one.
- */
- public LemmaSet copy()
- {
+
+ /**
+ * Returns a new lemma set containing exactly the same set of formulas as
+ * this one.
+ */
+ public LemmaSet copy() {
LemmaSet ret = new LemmaSet(ctxt);
-
+
ListIterator i = formulas.listIterator();
- while(i.hasNext())
- ret.addLemma((Expr)i.next());
-
+ while (i.hasNext())
+ ret.addLemma((Expr) i.next());
+
return ret;
}
-
- public Expr simplify(Expr e)
- {
+
+ public Expr simplify(Expr e) {
Expr e_ = null;
-
- while (e_ != e)
- {
+
+ while (e_ != e) {
e_ = e;
-
+
if (e.construct == Expr.TERM_APP) {
- TermApp ta = (TermApp)e;
-
+ TermApp ta = (TermApp) e;
+
if (ta.head.construct == Expr.CONST) {
- Const c = (Const)ta.head;
- if (ctxt.isTermCtor(c))
- break;
+ Const c = (Const) ta.head;
+ if (ctxt.isTermCtor(c))
+ break;
}
}
if (e.construct == Expr.MATCH) {
- Match m = (Match)e;
+ Match m = (Match) e;
Expr mt_ = simplify(m.t);
if (mt_ != m.t) {
- e = new Match(
- simplify(m.t),
- m.x1,
- m.x2,
- m.T,
- m.C,
- m.consume_scrut
- );
- }
- }
-
+ e = new Match(simplify(m.t), m.x1, m.x2, m.T, m.C,
+ m.consume_scrut);
+ }
+ }
+
e = rewrite(e);
e = e.evalStep(ctxt);
}
-
+
return e;
}
-
-
- public Expr instantiate(Expr e)
- {
+
+ public Expr instantiate(Expr e) {
Expr ret = e;
-
+
ListIterator i = formulas.listIterator();
- while(i.hasNext()) {
- Expr curr = (Expr)i.next();
-
+ while (i.hasNext()) {
+ Expr curr = (Expr) i.next();
+
if (curr.construct != Expr.ATOM)
continue;
-
- Atom a = (Atom)curr;
-
+
+ Atom a = (Atom) curr;
+
if (a.equality == false)
continue;
-
+
if (a.Y1.construct == Expr.VAR) {
- if (a.Y2.construct == Expr.TERM_APP) {
- TermApp ta = (TermApp)a.Y2;
-
- if (ta.head.construct == Expr.CONST &&
ctxt.isTermCtor((Const)ta.head))
+ if (a.Y2.construct == Expr.TERM_APP) {
+ TermApp ta = (TermApp) a.Y2;
+
+ if (ta.head.construct == Expr.CONST
+ && ctxt.isTermCtor((Const) ta.head))
ret = ret.subst(a.Y2, a.Y1);
- }
- else if(a.Y2.construct == Expr.CONST) {
+ } else if (a.Y2.construct == Expr.CONST) {
ret = ret.subst(a.Y2, a.Y1);
}
- }
- else if (a.Y2.construct == Expr.VAR) {
- if (a.Y1.construct == Expr.TERM_APP) {
- TermApp ta = (TermApp)a.Y1;
-
- if (ta.head.construct == Expr.CONST &&
ctxt.isTermCtor((Const)ta.head))
+ } else if (a.Y2.construct == Expr.VAR) {
+ if (a.Y1.construct == Expr.TERM_APP) {
+ TermApp ta = (TermApp) a.Y1;
+
+ if (ta.head.construct == Expr.CONST
+ && ctxt.isTermCtor((Const) ta.head))
ret = ret.subst(a.Y1, a.Y2);
- }
- else if(a.Y1.construct == Expr.CONST)
+ } else if (a.Y1.construct == Expr.CONST)
ret = ret.subst(a.Y1, a.Y2);
}
}
-
+
return ret;
- }
-
- public Expr rewrite(Expr e)
- {
+ }
+
+ public Expr rewrite(Expr e) {
ListIterator i = formulas.listIterator();
- while(i.hasNext()) {
- Expr curr = (Expr)i.next();
-
+ while (i.hasNext()) {
+ Expr curr = (Expr) i.next();
+
if (curr.construct != Expr.ATOM)
continue;
-
- Atom a = (Atom)curr;
-
+
+ Atom a = (Atom) curr;
+
if (a.equality == false)
continue;
-
+
+ // we may need to use both side of the equation to rebuild
+ // annotations... for example, { l = nil }. nil needs a type
+ // parameter, but the only way to deduce this is to look at
+ // the type of nil.
+
if (a.Y1.defEq(ctxt, e)) {
- if (a.Y2.construct == Expr.TERM_APP)
- {
- TermApp ta = (TermApp)a.Y2;
-
- if (ta.head.construct == Expr.CONST &&
ctxt.isTermCtor((Const)ta.head))
- return ta;
- }
- else if(a.Y2.construct == Expr.CONST)
- {
- return a.Y2;
+ Expr annY1 = UnjoinBase.RebuildAnnotations(a.Y1, ctxt);
+ ;
+
+ // we use the type of the lhs to reconstruct specificational
+ // arguments in the rhs. Is this sound? I think it is,
+ // because we are using the rhs to replace the lhs, so we
+ // really only care about the type of the lhs.
+ Expr tyY1 = annY1.classify(ctxt);
+
+ if (a.Y2.construct == Expr.TERM_APP) {
+ TermApp ta = (TermApp) a.Y2;
+
+ if (ta.head.construct == Expr.CONST
+ && ctxt.isTermCtor((Const) ta.head)) {
+ Expr headTy = ta.head.classify(ctxt);
+
+ return UnjoinBase.RebuildAnnotationsTargeted(a.Y2,
+ tyY1, ctxt);
+ }
+ } else if (a.Y2.construct == Expr.CONST) {
+ if (ctxt.isTermCtor((Const) a.Y2))
+ return UnjoinBase.RebuildAnnotationsTargeted(a.Y2,
+ tyY1, ctxt);
}
}
-
+
if (a.Y2.defEq(ctxt, e) && a.Y1.construct == Expr.TERM_APP) {
- if (a.Y1.construct == Expr.TERM_APP)
- {
- TermApp ta = (TermApp)a.Y1;
-
- if (ta.head.construct == Expr.CONST &&
ctxt.isTermCtor((Const)ta.head))
- return ta;
- }
- else if(a.Y1.construct == Expr.CONST)
- {
- return a.Y1;
+ Expr annY2 = UnjoinBase.RebuildAnnotations(a.Y2, ctxt);
+
+ // we use the type of the lhs to reconstruct specificational
+ // arguments in the rhs. Is this sound? I think it is,
+ // because we are using the rhs to replace the lhs, so we
+ // really only care about the type of the lhs.
+ Expr tyY2 = annY2.classify(ctxt);
+
+ if (a.Y1.construct == Expr.TERM_APP) {
+ TermApp ta = (TermApp) a.Y1;
+
+ if (ta.head.construct == Expr.CONST
+ && ctxt.isTermCtor((Const) ta.head))
+ return UnjoinBase.RebuildAnnotationsTargeted(ta, tyY2,
+ ctxt);
+ } else if (a.Y1.construct == Expr.CONST) {
+ if (ctxt.isTermCtor((Const) a.Y1))
+ return UnjoinBase.RebuildAnnotationsTargeted(a.Y1,
+ tyY2, ctxt);
}
}
}
-
+
return e;
}
}
=======================================
--- /branches/1.0/guru/Match.java Mon Nov 21 12:42:14 2011
+++ /branches/1.0/guru/Match.java Mon Nov 28 13:07:03 2011
@@ -191,22 +191,13 @@
if (isConstructorTerm)
isConstructorTerm &= baseCtxt.isTermCtor( (Const)((TermApp)t_).head
);
- if (isConstructorTerm) {
- if (((TermApp)t_).head != c.c)
- continue;
- }
- else if (t_.construct == CONST) {
- if (t_ != c.c)
- continue;
- }
-
// Prepend immediate deductions onto case body deductions -----
if (c.x.length == 0) {
-
+
if (!UnjoinBase.plausible(t_, c.c, uctxt, baseCtxt,true))
continue;
- Atom matchEq = new Atom(true, t_, c.c);
+ Expr matchEq = (new Atom(true, t_, c.c)).dropAnnos(baseCtxt);
Var matchEqVar = new Var("p" + uctxt.proofCounter);
if (t_.construct != CONST)
@@ -232,6 +223,9 @@
}
else {
+ if (!UnjoinBase.plausible(t_, new TermApp(c.c,c.x), uctxt,
baseCtxt,true))
+ continue;
+
Expr body = c.body;
// Create argument variables -----
@@ -249,28 +243,46 @@
);
}
else {
- FunType consType =
(FunType)c.c.classify(baseCtxt).defExpandTop(baseCtxt);
-
- Var[] clones = new Var[consType.vars.length];
- Var[] nonSpecificationalClones = new Var[c.x.length];
+ FunType consType =
(FunType)c.c.classify(baseCtxt);//.defExpandTop(baseCtxt);
+ Expr scrutType = t_.classify(baseCtxt);
+
+ assert(consType.vars.length == c.x.length);
+
+ Expr[] clones = new Expr[consType.vars.length];
+ boolean[] isConcrete = new boolean[consType.vars.length];
Expr[] types = new Expr[consType.vars.length];
int last = consType.vars.length-1;
//index into non-specificational args
int uInd = 0;
+ HashMap varMap = new HashMap();
+ UnjoinBase.InferVars(varMap, consType.body, scrutType);
+
for(int j = 0; j < clones.length; ++j)
- {
- String name;
- if (t_.construct == VAR)
- name = ((Var)t_).name + j;
+ {
+ if (varMap.containsKey(consType.vars[0]))
+ {
+ clones[j] = (Expr)varMap.get(consType.vars[0]);
+ types[j] = clones[j].classify(baseCtxt);
+ isConcrete[j] = true;
+ }
else
- name = "c" + j;
-
- clones[j] = new Var(name);
- types[j] = consType.types[0];
- baseCtxt.setClassifier(clones[j], types[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];
+ isConcrete[j] = false;
+ }
+
+ baseCtxt.setClassifier((Var)clones[j], types[j]);
+
+ /*
int spec = (consType.owned[0].status & Ownership.SPEC);
if (!(clones[j].isTypeOrKind(baseCtxt) ||
@@ -281,23 +293,31 @@
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.
+ // we're doing something similar in lemma set,
+ // should we factor this out?
if (j != last)
consType = (FunType)consType.instantiate(clones[j]);
}
-
- Atom matchEq = new Atom(
+ Expr consTypeResult =
consType.instantiate(clones[clones.length-1]);
+
+ for (int j = clones.length-1; j >= 0; --j)
+ body = body.subst(clones[j], c.x[j]);
+
+ Expr matchEq = new Atom(
true,
t_,
- new TermApp(c.c,nonSpecificationalClones)
- );
+ new TermApp(c.c,clones)
+ ).dropAnnos(baseCtxt);
Var matchEqVar = new Var("p" + uctxt.proofCounter);
baseCtxt.setClassifier(matchEqVar, matchEq);
+
uctxt.proofCounter++;
uctxt.lemmaSet.addLemma(matchEq);
@@ -313,10 +333,13 @@
uctxt.lemmaSet.removeLemma(matchEq);
//prepend immediate deductions to case body deductions
- branch = new UnjoinIntro(matchEqVar, matchEq, branch);
-
- for (int j = types.length-1; j >= 0; --j)
- branch = new UnjoinIntro(clones[j], types[j], branch);
+ branch = new UnjoinIntro(matchEqVar,
matchEq.dropAnnos(baseCtxt), branch);
+
+ for (int j = clones.length-1; j >= 0; --j)
+ {
+ if (!isConcrete[j])
+ branch = new UnjoinIntro((Var)clones[j], types[j], branch);
+ }
}
}
=======================================
--- /branches/1.0/guru/UnjoinBase.java Mon Nov 21 12:42:14 2011
+++ /branches/1.0/guru/UnjoinBase.java Mon Nov 28 13:07:03 2011
@@ -4,6 +4,9 @@
import java.util.List;
import java.util.Stack;
import java.util.Vector;
+import java.util.Map;
+import java.util.Map.Entry;
+import java.util.HashMap;
public abstract class UnjoinBase extends Expr {
@@ -34,14 +37,415 @@
class VarValue
{
public final Var var;
- public final Expr classifier;
-
- public VarValue(Var var, Expr classifier)
+ public final Expr value;
+
+ public VarValue(Var var, Expr value)
{
this.var = var;
- this.classifier = classifier;
+ this.value = value;
}
}
+
+ // Not sure how robust this is... might have to revisit it.
+ static public void InferVars(HashMap varMap, Expr abstr, Expr concrete)
+ {
+ switch (abstr.construct)
+ {
+ case TYPE_APP:
+ assert(concrete.construct == TYPE_APP);
+ TypeApp taAbstr = (TypeApp)abstr;
+ TypeApp taConcrete = (TypeApp)concrete;
+ assert(taAbstr.X.length == taConcrete.X.length);
+
+ for (int i = 0; i < taAbstr.X.length; ++i)
+ InferVars(varMap, taAbstr.X[i], taConcrete.X[i]);
+
+ break;
+ case TERM_APP:
+ assert(concrete.construct == TERM_APP);
+ TermApp termAppAbstr = (TermApp)abstr;
+ TermApp termAppConcrete = (TermApp)concrete;
+
+ assert(termAppAbstr.X.length == termAppConcrete.X.length);
+ assert(termAppAbstr.head == termAppConcrete.head);
+
+ for (int i = 0; i < termAppAbstr.X.length; ++i)
+ InferVars(varMap, termAppAbstr.X[i], termAppConcrete.X[i]);
+
+ break;
+ case VAR:
+ if (abstr != concrete)
+ varMap.put(abstr, concrete);
+ break;
+ case CONST:
+ break;
+ case FUN_TYPE:
+ assert(concrete.construct == FUN_TYPE);
+ FunType ftAbstr = (FunType)abstr;
+ FunType ftConcrete = (FunType)concrete;
+
+ assert(ftAbstr.vars.length == ftConcrete.vars.length);
+
+ for(int i = 0; i < ftAbstr.vars.length; ++i)
+ {
+ InferVars(varMap, ftAbstr.vars[0], ftConcrete.vars[0]);
+
+ if (i != (ftAbstr.vars.length-1))
+ {
+ //maybe I should instantiate these with null instead.
+ //this is closely coupled with the case for Var.
+ ftAbstr = (FunType)ftAbstr.instantiate(ftConcrete.vars[0]);
+ ftConcrete = (FunType)ftConcrete.instantiate(ftConcrete.vars[0]);
+ }
+ }
+
+ Expr instAbstr = ftAbstr.instantiate(ftConcrete.vars[0]);
+ Expr instConcrete = ftConcrete.instantiate(ftConcrete.vars[0]);
+
+ InferVars(varMap, instAbstr,instConcrete);
+
+ break;
+ default:
+ // I think you are allowed to have any terms in type apps,
+ // but I have only seen those listed above.
+ assert(false);
+ }
+ }
+
+ public Expr InferType(Expr t, Context ctxt)
+ {
+ switch (t.construct)
+ {
+ case Expr.TERM_APP:
+ Expr annotatedApp = RebuildAnnotations((TermApp)t, ctxt);
+ return annotatedApp.classify(ctxt);
+ case Expr.VAR:
+ return ctxt.getClassifier((Var)t);
+ case Expr.CONST:
+ return ctxt.getClassifier((Const)t);
+ default:
+ // A precondition for this function is that t is a term
+ // containing only the above constructs.
+ assert(false);
+ return null;
+ }
+ }
+
+ public static Expr RebuildAnnotations(
+ Expr uTerm,
+ Context ctxt
+ )
+ {
+ HashMap varMap = new HashMap();
+ Expr rebuilt = RebuildAnnotationsAux(varMap, uTerm, ctxt);
+ rebuilt = substitute(varMap, rebuilt);
+ return rebuilt;
+ }
+
+ public static Expr RebuildAnnotationsAux(HashMap varMap, Expr uTerm,
Context ctxt)
+ {
+ if (uTerm.construct == TERM_APP) {
+ TermApp ta = (TermApp)uTerm;
+
+ FunType ty = (FunType)ta.head.classify(ctxt);
+
+ return RebuildAnnotationsTargetedAux(varMap, uTerm, ty.body, ctxt);
+ }
+ else if (uTerm.construct == CONST) {
+ Const c = (Const)uTerm;
+
+ if(!ctxt.isCtor(c))
+ return c;
+
+ Expr termTy = c.classify(ctxt);
+ if(termTy.construct != Expr.FUN_TYPE)
+ return c;
+
+ FunType ty = (FunType)termTy;
+ return RebuildAnnotationsTargetedAux(varMap, uTerm, ty.body, ctxt);
+ }
+ else if (uTerm.construct == VAR) {
+ return uTerm;
+ }
+ else {
+ // A precondition to this function is that the term
+ // consists solely of TermApps, Consts, and Vars
+ assert(false);
+ return null;
+ }
+ }
+
+ public static Expr substitute(HashMap subs, Expr target)
+ {
+ if (target.construct == TERM_APP) {
+ TermApp ta = (TermApp)target;
+
+ Expr[] X = new Expr[ta.X.length];
+ for (int i = 0; i < ta.X.length; ++i)
+ X[i] = substitute(subs, ta.X[i]);
+
+ return new TermApp(ta.head, X);
+ }
+ else if (target.construct == CONST) {
+ return target;
+ }
+ else if (target.construct == VAR) {
+ Expr sub = (Expr)subs.get(target);
+ return (sub != null) ? sub : target;
+ }
+ else {
+ // A precondition to this function is that the term
+ // consists solely of TermApps, Consts, and Vars
+ assert(false);
+ return null;
+ }
+ }
+
+ public static Expr RebuildAnnotationsTargeted(
+ Expr uTerm,
+ Expr targetTy,
+ Context ctxt
+ )
+ {
+ HashMap varMap = new HashMap();
+ Expr rebuilt = RebuildAnnotationsTargetedAux(varMap, uTerm, targetTy,
ctxt);
+ rebuilt = substitute(varMap, rebuilt);
+ return rebuilt;
+ }
+
+ //
+ //
+ public static Expr RebuildAnnotationsTargetedAux(
+ HashMap varMap,
+ Expr uTerm,
+ Expr targetTy,
+ Context ctxt
+ )
+ {
+ if (uTerm.construct == TERM_APP) {
+ TermApp ta = (TermApp)uTerm;
+
+ // TODO: One more case I really think this strategy is going to work...
+ // keep at it!
+ //
+ FunType ftHead = (FunType)ta.head.classify(ctxt);
+
+ HashMap subs = new HashMap();
+ InferVars(subs, ftHead.body, targetTy);
+
+ FunType ftHead2 = ftHead;
+
+ Var[] vars2 = new Var[ftHead.vars.length];
+ for (int i = 0; i < vars2.length; ++i)
+ {
+ Expr sub = (Expr)subs.get(ftHead2.vars[i]);
+
+ //TODO: the var classifiers aren't going to match the types.
+ //but does it matter? They should match (look at VarListExp.subst)
+ if (sub != null)
+ ftHead2 = (FunType)ftHead2.subst(sub, ftHead.vars[i]);
+ }
+
+ Expr[] X = new Expr[ftHead2.vars.length];
+ int uInd = 0;
+ for(int i = 0; i < ftHead2.vars.length; ++i)
+ {
+ boolean spec;
+ spec = ftHead2.owned[i].status == Ownership.SPEC;
+
+ if (!(ftHead2.vars[i].isTypeOrKind(ctxt) ||
+ ftHead2.vars[i].isProof(ctxt) ||
+ spec) ) {
+
+ X[i] = RebuildAnnotationsTargetedAux(
+ varMap,
+ ta.X[uInd],
+ ftHead2.types[i],
+ ctxt
+ );
+
+ uInd++;
+ }
+ else
+ {
+ X[i] = ftHead2.vars[i];
+ }
+ }
+
+ return new TermApp(ta.head, X);
+ }
+ else if (uTerm.construct == CONST) {
+ Const c = (Const)uTerm;
+
+ if(!ctxt.isCtor(c))
+ {
+ InferVars(varMap, targetTy, c.classify(ctxt));
+ return c;
+ }
+
+ Expr headTy = c.classify(ctxt);
+ if(headTy.construct != Expr.FUN_TYPE)
+ {
+ InferVars(varMap, targetTy, c.classify(ctxt));
+ return c;
+ }
+
+ FunType ft = (FunType)headTy;
+ HashMap subs = new HashMap();
+ InferVars(subs, ft.body, targetTy);
+
+ Var[] vars = new Var[ft.vars.length];
+
+ // Inherited specificational vars are used rather than those from
+ // the constructor type so that we keep track of as few vars as
possible.
+ for (int i = 0; i < ft.vars.length; ++i)
+ {
+ vars[i] = (Var)subs.get(ft.vars[i]);
+ assert(vars[i] != null);
+ }
+
+ return new TermApp(c, vars);
+ }
+ else if (uTerm.construct == VAR) {
+ Expr varTy = uTerm.classify(ctxt);
+ InferVars(varMap, varTy, targetTy);
+ return uTerm;
+ }
+ else {
+ // A precondition to this function is that the term
+ // consists solely of TermApps, Consts, and Vars
+ assert(false);
+ return null;
+ }
+ }
+
+ /*
+ public Expr RebuildAnnotations(HashMap varMap, Expr uTerm, Context ctxt)
+ {
+ if (uTerm.construct == FUN_TERM) {
+ TermApp uApp = (TermApp)uTerm;
+ FunType ft = (FunType)uApp.head.classify(ctxt);
+
+ Expr[] X = uApp.X;
+ int uInd = 0;
+
+ Vector values = new Vector();
+
+ for (int i = 0; i < ft.vars.length; ++i) {
+ boolean spec = (ft.owned[i].status & (1<<Ownership.SPEC)) != 0;
+
+ if (!(ft.vars[i].isTypeOrKind(ctxt) ||
+ ft.vars[i].isProof(ctxt) ||
+ spec) ) {
+
+
+ assert(uApp.X[uInd].construct == TERM_APP ||
+ uApp.X[uInd].construct == VAR ||
+ uApp.X[uInd].construct == CONST);
+
+ // Rebuilding to the best of our abilities at this point
+ // may leave out items which are deduced from other
+ // arguments, but it is done for the purpose of extracting all
+ // of the useful data we need. A full rebuild happens later.
+ Expr rebuiltArg;
+ if (uApp.X[uInd].construct == TERM_APP)
+ rebuiltArg = RebuildAnnotations(varMap, (TermApp)uApp.X[uInd],
ctxt);
+ else
+ rebuiltArg = uApp.X[uInd];
+
+ varMap.put(ft.vars[i], rebuiltArg);
+ InferVars(varMap, ft.types[i], rebuiltArg.classify(ctxt));
+
+ uInd++;
+ }
+ }
+
+ Expr[] retArgs = new Expr[ft.vars.length];
+
+ for(int i = 0; i < retArgs.length; ++i) {
+ retArgs[i] = RebuildAnnotations(
+ varMap,
+ (Expr)varMap.get(ft.vars[i]),
+ ctxt
+ );
+ }
+
+ return new TermApp(uApp.head, retArgs);
+ }
+ else if (uTerm.construct == CONST)
+ {
+ Expr termTy = uTerm.classify(ctxt);
+ if(termTy.construct != Expr.FUN_TYPE)
+ return uTerm;
+
+ UnjoinBase.InferVars(varMap, ((FunType)termTy).body, targetTy);
+
+ FunType ftTermTy = (FunType)termTy;
+
+ retArgs = new Expr[ftTermTy.vars.length];
+
+ for(int i = 0; i < retArgs.length; ++i) {
+ retArgs[i] = (Expr)varMap.get(ftTermTy.vars[i]);
+ assert(retArgs[i] != null);
+ }
+
+ return new TermApp(uterm, retArgs);
+ }
+ else if (uTerm.construct == VAR)
+ {
+
+ }
+ else
+ {
+ assert(false);
+ return null;
+ }
+ }
+
+ public static Expr RebuildAnnotations(TermApp uApp, Expr targetTy,
Context ctxt)
+ {
+ FunType ft = (FunType)uApp.head.classify(ctxt);
+
+ Expr[] X = uApp.X;
+ int uInd = 0;
+
+ Vector values = new Vector();
+ HashMap varMap = new HashMap();
+
+ for (int i = 0; i < ft.vars.length; ++i) {
+ boolean spec = (ft.owned[i].status & (1<<Ownership.SPEC)) != 0;
+
+ if (!(ft.vars[i].isTypeOrKind(ctxt) ||
+ ft.vars[i].isProof(ctxt) ||
+ spec) ) {
+
+
+ assert(uApp.X[uInd].construct == TERM_APP ||
+ uApp.X[uInd].construct == VAR ||
+ uApp.X[uInd].construct == CONST);
+
+ Expr rebuiltArg;
+ if (uApp.X[uInd].construct == TERM_APP)
+ rebuiltArg = RebuildAnnotations((TermApp)uApp.X[uInd], ctxt);
+ else
+ rebuiltArg = uApp.X[uInd];
+
+ varMap.put(ft.vars[i], rebuiltArg);
+ InferVars(varMap, ft.types[i], rebuiltArg.classify(ctxt));
+
+ uInd++;
+ }
+ }
+
+ Expr[] retArgs = new Expr[ft.vars.length];
+
+ for(int i = 0; i < retArgs.length; ++i) {
+ retArgs[i] = (Expr)varMap.get(ft.vars[i]);
+ }
+
+ return new TermApp(uApp.head, retArgs);
+ }
+ */
public static boolean plausible(
Expr term,
@@ -93,7 +497,7 @@
if (taTerm.head.eval(baseCtxt).construct != Expr.FUN_TERM)
return true; // maybe it could be a variable
- FunTerm inst = (FunTerm)taTerm.head.eval(baseCtxt);
+ FunTerm inst =
(FunTerm)taTerm.head.defExpandTop(baseCtxt,false,true);
Var oldRec = uCtxt.recVar;
uCtxt.recVar = inst.r;
@@ -171,7 +575,7 @@
if (!scrutPlausible)
continue;
- Atom matchEq = new Atom(true, t_, c.c);
+ Expr matchEq = (new Atom(true, t_, c.c)).dropAnnos(baseCtxt);
Var matchEqVar = new Var("p");
if (t_.construct != Expr.CONST)
@@ -203,7 +607,9 @@
if (!scrutPlausible)
continue;
-
+
+
+
if (isScrutConstructor)
{
TermApp ta = (TermApp)t_;
@@ -225,7 +631,26 @@
//
Expr substitutedBody = c.body;;
+ Expr scrutClassifier = t_.classify(baseCtxt);
FunType consType =
(FunType)c.c.classify(baseCtxt).defExpandTop(baseCtxt);
+
+ HashMap varMap = new HashMap();
+ //TODO: I can't remember why I did this. Is this necessary
+ //for plausibility?
+ InferVars(varMap, consType.body, scrutClassifier);
+
+ for (int j = 0; j < consType.vars.length; ++j)
+ {
+ Expr sub = (Expr)varMap.get(consType.vars[j]);
+ if (sub != null)
+ {
+ Var newVar = new Var(c.x[j].name);
+ baseCtxt.setClassifier(newVar, sub);
+
+ substitutedBody = substitutedBody.subst(newVar, c.x[j]);
+ }
+ }
+
Var[] clones = new Var[consType.vars.length];
Var[] nonSpecificationalClones = new Var[c.x.length];
Expr[] types = new Expr[consType.vars.length];
@@ -241,11 +666,11 @@
types[j] = consType.types[0];
baseCtxt.setClassifier(clones[j], types[j]);
- int spec = (consType.owned[0].status & Ownership.SPEC);
+ boolean spec = (consType.owned[0].status == Ownership.SPEC);
if (!(clones[j].isTypeOrKind(baseCtxt) ||
clones[j].isProof(baseCtxt) ||
- spec != 0) ) {
+ spec) ) {
nonSpecificationalClones[uInd] = clones[j];
substitutedBody = substitutedBody.subst(clones[j],
c.x[uInd]);
@@ -257,12 +682,12 @@
if (j != last)
consType = (FunType)consType.instantiate(clones[j]);
}
-
- Atom matchEq = new Atom(
+
+ Expr matchEq = new Atom(
true,
t_,
- new TermApp(c.c,nonSpecificationalClones)
- );
+ new TermApp(c.c,clones)
+ ).dropAnnos(baseCtxt);
uCtxt.lemmaSet.addLemma(matchEq);
@@ -581,6 +1006,41 @@
return null;
case Expr.ABORT:
+ return null;
+ case Expr.ABBREV:
+ Abbrev a = (Abbrev)e;
+ lift = liftSingleMatch(a.U);
+
+ if (lift != null) {
+ return new LiftedMatch(
+ lift.scrut,
+ lift.hole,
+ lift.cases,
+ new Abbrev(
+ a.flags,
+ a.x,
+ lift.context,
+ a.G
+ )
+ );
+ }
+
+ lift = liftSingleMatch(a.U);
+
+ if (lift != null) {
+ return new LiftedMatch(
+ lift.scrut,
+ lift.hole,
+ lift.cases,
+ new Abbrev(
+ a.flags,
+ a.x,
+ a.U,
+ lift.context
+ )
+ );
+ }
+
return null;
default:
assert(false);
@@ -620,6 +1080,9 @@
return matchFree(let.t1) && matchFree(let.t2);
case Expr.ABORT:
return true;
+ case Expr.ABBREV:
+ Abbrev a = (Abbrev)e;
+ return matchFree(a.G) && matchFree(a.U);
default:
assert(false);
return false;
@@ -715,7 +1178,10 @@
if (lhs.construct != TERM_APP)
return lhs;
- Expr lhs2 = lhs;
+ //TODO: generate an error if lhs has anything other than
+ //term apps, variables, and constants.
+
+ Expr lhs2 = RebuildAnnotations((TermApp)lhs, ctxt);
while (true) {
//System.out.println("a.");
@@ -741,17 +1207,17 @@
// The pre-instantiated value of the head.
Const c = (Const)ta.head;
- // A variable used to instantiate the head
- Expr ev = c.eval(ctxt);
+ // Def expand the head without dropping annotations.
+ Expr ev = c.defExpandTop(ctxt, false, true);
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"
- );
+ "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 head: " + ev.toString(ctxt) + "\n"
+ );
}
FunTerm inst = (FunTerm)ev;
=======================================
--- /branches/1.0/tests/unjoin.g Mon Nov 21 12:42:14 2011
+++ /branches/1.0/tests/unjoin.g Mon Nov 28 13:07:03 2011
@@ -4,12 +4,49 @@
Include "../lib/minus.g"
Include "../lib/vec.g"
Include "../lib/minmax.g"
-
-
+Include "../../versat/src/lib_includes.g"
+Include "../../versat/src/cnf-lemma.g"
+
+Define matchLet :=
+ fun(x : nat)(y : bool).
+ match x with
+ | Z =>
+ tt
+ | S n' =>
+ let z = (and y tt) in
+ z
+ end.
+
+Define matchLetProof
+ : Forall(x : nat)(y: bool)(u1 : { (matchLet x y) = tt })
+ (x' : nat)(u2 : { x = (S x')}). { y = tt }
+:=
+ foralli(x : nat)(y: bool)(u1 : { (matchLet x y) = tt })
+ (x' : nat)(u2 : { x = (S x')}).
+ lemma u2 in
+ unjoin u1 with
+ | foralli(p0 : { (and y tt) = tt }).
+ unjoin p0 with
+ | foralli(u : {y = tt}).
+ u
+ end
+ end.
+
Inductive list2 : Fun(A:type).type :=
| nil2 : Fun(A:type).<list2 A>
| cons2 : Fun(A:type)(a:A)(l:<list2 A>). <list2 A>.
+Define length_eq_Z2
+ : Forall(A:type)(l:<list A>)
+ (u:{ (length l) = Z}).
+ { l = nil } :=
+ foralli(A:type)(l:<list A>)
+ (u:{ (length l) = Z}).
+ unjoin u with
+ | foralli(p0 : { l = nil }).
+ p0
+ end.
+
Define matchArgs :=
fun(x : nat)(y : nat).
let z =
@@ -60,39 +97,148 @@
+
+Define eqlistEq2 : Forall(A:type)
+ (l1 l2:<list A>)
+ (eqA:Fun(x1 x2:A).bool)
+ (eqA_total:Forall(x1 x2:A).Exists(o:bool).{ (eqA
x1 x2) = o })
+ (eqA_eq:Forall(x1 x2:A)(u:{ (eqA x1 x2) = tt }).{
x1 = x2 })
+ (u:{ (eqlist eqA l1 l2) = tt }). { l1 = l2 } :=
+
+ foralli(A:type).
+ induction(l1:<list A>) by l1_eq l1_Eq IHl1
+ return Forall(l2:<list A>)
+ (eqA:Fun(x1 x2:A).bool)
+ (eqA_total:Forall(x1 x2:A).Exists(o:bool).{ (eqA x1 x2) =
o })
+ (eqA_eq:Forall(x1 x2:A)(u:{ (eqA x1 x2) = tt }).{ x1 = x2
})
+ (u:{ (eqlist eqA l1 l2) = tt }).
+ { l1 = l2 }
+ with
+ | nil _ =>
+ foralli(l2 : <list A>)(eqA:Fun(x1 x2:A).bool)
+ (eqA_total:Forall(x1 x2:A).Exists(o:bool).{ (eqA x1 x2) = o })
+ (eqA_eq:Forall(x1 x2:A)(u:{ (eqA x1 x2) = tt }).{ x1 = x2 })
+ (u:{ (eqlist eqA l1 l2) = tt }).
+
+ lemma l1_eq in
+ unjoin u with
+ | foralli(p0 : { l2 = nil }).
+ hypjoin l1 l2 by l1_eq p0 end
+ end
+ | cons _ h1 t1 =>
+ foralli(l2 : <list A>)(eqA:Fun(x1 x2:A).bool)
+ (eqA_total:Forall(x1 x2:A).Exists(o:bool).{ (eqA x1 x2) = o })
+ (eqA_eq:Forall(x1 x2:A)(u:{ (eqA x1 x2) = tt }).{ x1 = x2 })
+ (u:{ (eqlist eqA l1 l2) = tt }).
+ lemma l1_eq in
+ unjoin u with
+ | foralli(l21 : A)(l22 : <list A>)
+ (p0 : { l2 = (cons l21 l22) })
+ (u : { (and (eqA h1 l21) (eqlist eqA t1 l22)) = tt }).
+ lemma
+ : { (eqlist eqA t1 l22) = tt }
+ [and_eq_tt2
+ terminates (eqA h1 l21) by eqA_total
+ terminates (eqlist A eqA t1 l22) by [eqlist_total A eqA
eqA_total t1 l22]
+ u
+ ]
+
+ : { (eqA h1 l21) = tt }
+ [and_eq_tt1
+ terminates (eqA h1 l21) by eqA_total
+ terminates (eqlist A eqA t1 l22) by [eqlist_total A eqA
eqA_total t1 l22]
+ u
+ ]
+ in
+ hypjoin l1 l2 by
+ : { h1 = l21 } [eqA_eq h1 l21 ##]
+ : { t1 = l22 } [IHl1 t1 l22 eqA eqA_total eqA_eq ##]
+ : { l2 = (cons l21 l22) } p0
+ : { l1 = (cons h1 t1) } l1_eq
+ end
+ end
+ end.
+
+
Define nth_append2 : Forall(A:type)(n:nat)(l:<list A>)(a:A)
(u:{(nth n l) = a}).
Exists(l1 l2:<list A>).
{ l = (append l1 (cons a l2)) } :=
- foralli(A:type)(n:nat)(l:<list A>)(a:A)
- (u:{(nth n l) = a}).
-
+ foralli(A:type).
+ induction (n: nat)
+ return Forall(l:<list A>)(a:A)(u:{(nth n l) = a}).
+ Exists(l1 l2:<list A>). { l = (append l1 (cons a l2)) }
+ with
+ | Z =>
+ foralli(l:<list A>)(a:A)(u:{(nth n l) = a}).
+ lemma n_eq in
+ unjoin u with
+ | foralli(l1 : A)(l2 : <list A>)(p0 : { l = (cons l1 l2) })
+ (u : { l1 = a }).
+
+ existsi (nil A)
+ Exists(e2 : <list A>). { l = (append * (cons a e2)) }
+ existsi l2
+ { l = (append nil (cons a *)) }
+ hypjoin l (append nil (cons a l2)) by
+ : { l = (cons l1 l2) } p0
+ : { l1 = a } u
+ end
+ end
+ | S n' =>
+ foralli(l:<list A>)(a:A)(u:{(nth n l) = a}).
+ lemma n_eq in
+ unjoin u with
+ | foralli(l1 : A)(l2 : <list A>)(p0 : { l = (cons l1 l2) })
+ (u : { (nth A n' l2) = a }).
+ abbrev q0 =
+ : Exists(l21 l22: <list A>). { l2 = (append l21 (cons a l22)) }
+ [n_IH n' l2 a u]
+ in
+
+ abbrev q1 =
+ : Forall(l21 l22: <list A>)(u : { l2 = (append l21 (cons a l22)) }).
+ Exists(v1 v2 : <list A>). { l = (append v1 (cons a v2)) }
+ foralli(l21 l22: <list A>)(u : { l2 = (append l21 (cons a l22)) }).
+ existsi (cons A l1 l21)
+ Exists(v2 : <list A>). { l = (append * (cons a v2)) }
+ existsi l22
+ { l = (append (cons l1 l21) (cons a *)) }
+ hypjoin l (append (cons l1 l21) (cons a l22)) by
+ : { l = (cons l1 l2) } p0
+ : { l2 = (append l21 (cons a l22)) } u
+ end
+ in
+
+ existse q0
+ q1
+ end
+ end.
+
+
+%-
unjoin u with
- | foralli(p0 : { n = Z })(l0 : type)(l1 : l0)(l2 : <list l0>)
+ | foralli(p0 : { n = Z })(l1 : A)(l2 : <list A>)
(p1 : { l = (cons l1 l2) })(u : { l1 = a }).
- %% darnit... there is no way to prove l0 = A.
- %% I need to lookup l0 from the type of l. even though u
- %% is unannotated, we should be able to find the type in
- %%
-
+ existsi (nil A)
+ Exists(e2 : <list A>). { l = (append * (cons a e2)) }
+ existsi l2
+ { l = (append nil (cons a *)) }
+ hypjoin l (append nil (cons a l2)) by
+ : { l = (cons l1 l2) } p1
+ : { l1 = a } u
+ end
+
+ | foralli(n0 : nat)(p0 : { n = (S n0) })(l1 : A)(l2 : <list A>)
+ (p1 : { l = (cons l1 l2) })(u : { (nth A n0 l2) = a }).
lemma
- : { l0 = A }
- l
+ : Exists(l2' : <list A>). { l = (append
in
- existsi (nil A)
- Exists(l'' : <list l0>)
-
- | foralli(n0 : nat)(p0 : { n = (S n0) })(l0 : type)(l1 : l0)
- (l2 : <list l0>)(p1 : { l = (cons l1 l2) })
- (u : { (nth n0 l2) = a }).
-
-
-
end.
-
-Define set_nth_other : Forall(A:type)(l:<list A>)(n m:nat)(b:A)
+-%
+Define set_nth_other2 : Forall(A:type)(l:<list A>)(n m:nat)(b:A)
(u:{ n != m }).
{ (nth n (set_nth m l b)) = (nth n l) } :=
foralli(A:type).
@@ -135,7 +281,6 @@
end
end.
-
Define foldr2
: Fun(S A : type)(acc : Fun(s : S)(a : A). S)(init : S)(l : <list2 A>). S
:=
@@ -148,37 +293,10 @@
(foldr2 S A acc s' l')
end.
-Define matchLet :=
- fun(x : nat)(y : bool).
- match x with
- | Z =>
- tt
- | S n' =>
- let z = (and y tt) in
- z
- end.
-
-Define matchLetProof
- : Forall(x : nat)(y: bool)(u1 : { (matchLet x y) = tt })
- (x' : nat)(u2 : { x = (S x')}). { y = tt }
-:=
- foralli(x : nat)(y: bool)(u1 : { (matchLet x y) = tt })
- (x' : nat)(u2 : { x = (S x')}).
- lemma u2 in
- unjoin u1 with
- | foralli(p0 : { (and y tt) = tt }).
- unjoin p0 with
- | foralli(u : {y = tt}).
- u
- end
- end.
-
Define ormap :=
fun(l : <list2 bool>).
(foldr2 bool bool or ff l).
-
-
Define eqnatEq3 : Forall(n:nat)(u:{(eqnat n Z) = tt}). { n = Z } :=
foralli(n: nat)(u:{(eqnat n Z) = tt}).
unjoin u with
@@ -259,9 +377,6 @@
u
end.
-
-
-
Define badSub :=
fun(x : nat).
x.
@@ -335,19 +450,6 @@
end
-%- this doesn't work because we are not (yet) able to use inequalities as
lemmas.
-
-Define neqEqnat2 : Forall(n m : nat)(u:{n != m}).{ (eqnat n m) = ff } :=
- foralli(n m : nat)(u:{n != m}).
- case (eqnat n m) by v ign with
- | ff =>
- v
- | tt =>
- lemma u in
- unjoin v contra { (eqnat n m) = ff }
- end.
--%
-
%- unjoin wouldn't help here... it could enable us to avoid induction,
but I think induction is more straightforward and compact.
@@ -426,100 +528,6 @@
-%
-%-
-Define vec_vecc_shift2 :
- Forall(A: type)
- (n: nat)
- (v: <vec A n>)
- (m: nat)
- (u: { (lt m n) = tt } )
- (a: A)
- .
- { (vec_get v m) = (vec_get (vecc a v) (S m)) }
- :=
- foralli(A: type)(n: nat)(v: <vec A n>)(m: nat)(u: { (lt m n) = tt } )
- (a: A).
-
- lemma
-
-
- unjoin u with
- | foralli(p10 : { m = Z })(b' : nat)(p9 : { n = (S b') }).
-
- | foralli(a' : nat)(p13 : { m = (S a') })(b' : nat)
- (p12 : { n = (S b') })(u : { (lt a' b') = tt }).
- end.
-
--%
-%-
-Define minus_lt2 : Forall
- (a b:nat)(u1:{ (le b a) = tt })(u2:{ (lt Z b) = tt }).{ (lt (minus a b)
a) = tt }
- :=
- foralli(a: nat).
- induction (b:nat) return
- Forall(u1:{ (le b a) = tt })(u2:{ (lt Z b) = tt }).{ (lt (minus a b)
a) = tt }
- with
- | Z =>
- foralli(u1:{ (le b a) = tt })(u2:{ (lt Z b) = tt }).
- lemma b_eq in
- unjoin u2 contra { (lt (minus a b) a) = tt }
- | S b' =>
- foralli(u1:{ (le b a) = tt })(u2:{ (lt Z b) = tt }).
- lemma b_eq in
- unjoin u1 with
- %-
- | foralli(p0 : { (lt b a) = ff })(u : { (eqnat b a) = tt }).
- hypjoin (lt (minus a b) a) tt by
- : { b = a } [eqnatEq b a u]
- : { (minus b b) = Z } [x_minus_x b]
- : { b = (S b') } b_eq
- end
- | foralli(p1 : { (lt b a) = tt }).
-
- % yeah -- this doesn't seem to help. I blame the lack
- % of theorems in the minus library.
- lemma
- : { (lt b' a) = tt }
- [ltlt_trans b' b a b'_lt_b p1]
-
- : { (le b' a) = tt }
- [lt_implies_le b' a ##]
-
- : { (lt (S (minus a (S b'))) a) = tt }
- hypjoin (lt (minus a b) a) tt by
- : { (minus a b') = (S (minus a (S b'))) } [minusS2 b' a ##]
- : { b = (S b') } ##
- : { (lt (minus a b') a) = tt } [b_IH b' b'_le_a z_lt_b']
- in
- -%
- end %u1
- end %ind
--%
-
-Define vec_append_assoc2 : Forall(A:type)(n1 : nat)(l1 : <vec A n1>)
- (n2 n3 : nat)(l2 : <vec A n2>)(l3 : <vec A n3>).
- { (vec_append (vec_append l1 l2) l3) =
- (vec_append l1 (vec_append l2 l3)) } :=
- foralli(A:type).
- induction(n1:nat)(l1:<vec A n1>) return
- Forall(n2 n3 : nat)(l2 : <vec A n2>)(l3 : <vec A n3>).
- { (vec_append (vec_append l1 l2) l3) = (vec_append l1 (vec_append l2
l3)) }
- with
- | vecn A' =>
- foralli(n2 n3 : nat)(l2 : <vec A n2>)(l3 : <vec A n3>).
- hypjoin (vec_append (vec_append l1 l2) l3) (vec_append l1 (vec_append
l2 l3)) by
- : { l1 = (vecn A') } l1_eq
- end
- | vecc A' n1' x' l1' =>
- foralli(n2 n3 : nat)(l2 : <vec A n2>)(l3 : <vec A n3>).
- hypjoin (vec_append (vec_append l1 l2) l3) (vec_append l1 (vec_append
l2 l3)) by
- : { (vec_append (vec_append l1' l2) l3) = (vec_append l1'
(vec_append l2 l3)) }
- [l1_IH n1' l1' n2 n3 l2 l3]
- : { l1 = (vecc x' l1') }
- l1_eq
- end
- end.
-
%- well... it helped with the first case at least.
and only a case split on the vector was necessary here.
Define vec_vecc_shift2 :
@@ -552,26 +560,24 @@
| foralli(m0 : nat)(p3 : { m = (S m0) })(u : { (lt m0 n') = tt }).
[n_IH n'
end
-
-
- %-
- case v with
- | vecn _ =>
- abbrev Z_neq_n =
- trans clash Z (S n')
- symm n_eq
- in
-
- contra
- trans inj <vec ** *> v_Eq
- Z_neq_n
-
- { (vec_get v m) = (vec_get v' (S m)) }
- | vecc _ restLen x rest =>
- hypjoin (vec_get v m) (vec_get v' (S m)) by v_eq end
- end
- -%
end.
-%
+Define null_terminated_nth_tail_implies_lt2 :
+ Forall(n:nat)(c:<vec ulit n>)
+ (i:nat)
+ (u:{ (null_terminated (vec_nth_tail c i)) = tt })
+ .{ (lt i n) = tt }
+ :=
+ foralli(n:nat)(c:<vec ulit n>)
+ (i:nat)
+ (u:{ (null_terminated (vec_nth_tail c i)) = tt })
+ .
+ case (lt i n) by q1 _ with
+ | ff =>
+ lemma q1 in
+ unjoin u contra { (lt i n) = tt }
+ | tt => q1
+ end.
+
Classify eqnatNeq2.