[guru-lang] r546 committed - fixed some bugs. added some tests.
guru...@googlecode.com
Author: kevinclancy0
Date: Mon Oct 31 13:11:32 2011
Log: fixed some bugs. added some tests.
http://code.google.com/p/guru-lang/source/detail?r=546
Modified:
/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/Var.java
/branches/1.0/tests/unjoin.g
=======================================
--- /branches/1.0/guru/LemmaSet.java Thu Oct 27 08:11:15 2011
+++ /branches/1.0/guru/LemmaSet.java Mon Oct 31 13:11:32 2011
@@ -3,7 +3,7 @@
import java.util.ArrayList;
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
@@ -15,10 +15,12 @@
*/
public class LemmaSet {
- // The context used to decide definitional equality
+ /** 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)
@@ -29,9 +31,10 @@
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.)
+ /** 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));
@@ -40,7 +43,7 @@
formulas.add(newLemma);
}
- // Removes a lemma from the set.
+ /** Removes a lemma from the set. */
public void removeLemma(Expr toRemove)
{
assert(toRemove.isFormula(ctxt));
@@ -49,7 +52,7 @@
formulas.remove(toRemove);
}
- // Returns true iff the given lemma is contained in this set.
+ /** Returns true iff the given lemma is contained in this set */
public boolean hasLemma(Expr lemma)
{
assert(lemma.isFormula(ctxt));
@@ -65,8 +68,9 @@
return false;
}
- // Returns a new lemma set containing exactly the same set of formulas as
- // this one.
+ /** Returns a new lemma set containing exactly the same set of formulas as
+ * this one.
+ */
public LemmaSet copy()
{
LemmaSet ret = new LemmaSet(ctxt);
@@ -86,8 +90,10 @@
{
e_ = e;
- if (e.construct == Expr.MATCH)
- {
+ if (e.construct == Expr.TERM_APP)
+ break;
+
+ if (e.construct == Expr.MATCH) {
Match m = (Match)e;
Expr mt_ = simplify(m.t);
if (mt_ != m.t) {
=======================================
--- /branches/1.0/guru/Let.java Thu Oct 27 08:11:15 2011
+++ /branches/1.0/guru/Let.java Mon Oct 31 13:11:32 2011
@@ -174,8 +174,8 @@
boolean eq
)
{
- return Unjoin(
- t2.subst(t1, x1),
+ return t2.subst(t1, x1).Unjoin(
+ target,
proofCount,
ctxt,
eq
=======================================
--- /branches/1.0/guru/Match.java Thu Oct 27 08:11:15 2011
+++ /branches/1.0/guru/Match.java Mon Oct 31 13:11:32 2011
@@ -169,9 +169,11 @@
{
UnjoinDeduction ret = UnjoinDeduction.contradiction;
- Expr t_ = t;
- while (t_.construct != TERM_APP && t_ != t_.evalStep(baseCtxt))
- t_ = t_.evalStep(baseCtxt);
+ Expr t_ = baseCtxt.lemmaSet.simplify(t);
+
+ //baseCtxt.lemmaSet.instantiate(t);
+ //while (t_.construct != TERM_APP && t_ != t_.evalStep(baseCtxt))
+ // t_ = t_.evalStep(baseCtxt);
//Set ret to the disjunction of the deductions that can be made from
//each branch.
=======================================
--- /branches/1.0/guru/TermApp.java Thu Oct 27 08:11:15 2011
+++ /branches/1.0/guru/TermApp.java Mon Oct 31 13:11:32 2011
@@ -521,17 +521,44 @@
boolean eq
)
{
- Atom introAtom = new Atom(eq, this, target);
-
- //since this is the final deduction, we can name it whatever we
- //want without introducing ambiguity.
- Var introVar = new Var("u");
-
- return new UnjoinIntro(
- introVar,
- introAtom,
- UnjoinDeduction.empty
- );
+ if (evalStep(baseCtxt) == this
&& !Unjoin.placeHolder(target,baseCtxt))
+ {
+ // A term constructor
+
+ if (target.construct != TERM_APP)
+ return eq ? UnjoinDeduction.contradiction :
UnjoinDeduction.empty;
+ else
+ {
+ UnjoinDeduction ret = UnjoinDeduction.empty;
+
+ for (int i = 0; i < X.length; ++i)
+ {
+ Atom introAtom = new Atom(eq, this, target);
+ Var introVar = new Var("u");
+
+ ret = new UnjoinIntro(
+ introVar,
+ introAtom,
+ ret
+ );
+ }
+
+ return ret;
+ }
+ }
+ else
+ {
+ // A function call
+ Atom introAtom = new Atom(eq, this, target);
+ Var introVar = new Var("u");
+
+ return new UnjoinIntro(
+ introVar,
+ introAtom,
+ UnjoinDeduction.empty
+ );
+ }
+
}
public guru.carraway.Expr toCarraway(Context ctxt) {
=======================================
--- /branches/1.0/guru/Unjoin.java Thu Oct 27 08:11:15 2011
+++ /branches/1.0/guru/Unjoin.java Mon Oct 31 13:11:32 2011
@@ -122,6 +122,17 @@
}
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.
@@ -155,10 +166,21 @@
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;
+
+ 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
@@ -202,8 +224,8 @@
if (f.r != null && pre.construct == CONST)
fullInstantiation = (Expr)fullInstantiation.subst((Const)pre, f.r);
-
- //TODO: substitute lets and abbrevs here?
+ //continue past lets and abbrevs
+ fullInstantiation = fullInstantiation.eval(ctxt);
if (fullInstantiation.construct != TERM_APP)
return fullInstantiation;
@@ -284,7 +306,6 @@
Expr instantiated = instantiate(ctxt, scrutinee.Y1);
- instantiated = ctxt.lemmaSet.instantiate(instantiated);
UnjoinDeduction deduction = instantiated.Unjoin(
scrutinee.Y2,
@@ -298,11 +319,13 @@
if (unjoinPaths.size() != paths.size()) {
//TODO: spit out error message, remove assert
DumpUnjoinPaths(unjoinPaths, ctxt);
- handleError(ctxt, "blaaarg!");
- assert(false);
- System.exit(0);
+ handleError(ctxt, "Unjoin paths do not match the computed paths" +
+ " listed above.");
}
+ if (unjoinPaths.size() == 0)
+ handleError(ctxt, "Unjoin has deduced a contradiction.");
+
return classifyPaths(unjoinPaths, ctxt);
}
=======================================
--- /branches/1.0/guru/Var.java Thu Oct 27 08:11:15 2011
+++ /branches/1.0/guru/Var.java Mon Oct 31 13:11:32 2011
@@ -163,18 +163,24 @@
boolean eq
)
{
- if (baseCtxt.isMacroDefined(this))
- {
+ if (baseCtxt.isMacroDefined(this)) {
//TODO: this should be removed... abbrevs should be substituted
//before unjoining.
return evalStep(baseCtxt).Unjoin(target, proofCount, baseCtxt, eq);
}
- else
- {
+ else {
if (target == this)
return eq ? UnjoinDeduction.empty : UnjoinDeduction.contradiction;
- else
- return eq ? UnjoinDeduction.contradiction : UnjoinDeduction.empty;
+ else {
+ Atom introAtom = new Atom(eq, this, target);
+ Var introVar = new Var("u");
+
+ return new UnjoinIntro(
+ introVar,
+ introAtom,
+ UnjoinDeduction.empty
+ );
+ }
}
}
=======================================
--- /branches/1.0/tests/unjoin.g Fri Oct 21 12:38:46 2011
+++ /branches/1.0/tests/unjoin.g Mon Oct 31 13:11:32 2011
@@ -3,6 +3,173 @@
Include "../lib/bool.g"
Include "../lib/minus.g"
Include "../lib/vec.g"
+Include "../lib/minmax.g"
+
+Define letFunc :=
+ fun (x : bool).
+ let x = (or x x) in
+ one.
+
+Define letProof1
+ : Forall(x:bool)(u: { (letFunc x) = two }). { Z = one }
+:=
+ foralli(x:bool)(u: { (letFunc x) = two }).
+ unjoin u contra { Z = one }.
+
+Define letIdentity :=
+ fun(x : bool).
+ let y = (or ff x) in
+ y.
+
+Define letIdProof
+ : Forall(x:bool)(u: { (letIdentity x) = tt }). { x = tt }
+:=
+ foralli(x:bool)(u: { (letIdentity x) = tt }).
+ unjoin u with
+ | foralli(u : { x = tt }).
+ u
+ 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 matchAbbrev :=
+ fun(x : nat)(y : bool).
+ match x with
+ | Z =>
+ tt
+ | S n' =>
+ abbrev z = (and y tt) in
+ z
+ end.
+
+Define matchAbbrevProof
+ : Forall(x : nat)(y: bool)(u1 : { (matchAbbrev x y) = tt })
+ (x' : nat)(u2 : { x = (S x')}). { y = tt }
+:=
+ foralli(x : nat)(y: bool)(u1 : { (matchAbbrev 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 testMult :=
+ fun(x : nat).
+ (mult x one).
+
+Define funnyId :=
+ fun(x : nat).
+ match x with
+ | Z =>
+ x
+ | S x' =>
+ x
+ end.
+
+Define funnyIdProof
+ : Forall(x x': nat)(u : { x = (S x') })(u' : { (funnyId x) = two } ). {
x = two }
+:=
+ foralli(x x': nat)(u : { x = (S x') })(u' : { (funnyId x) = two } ).
+ lemma u in
+ unjoin u' with
+ | foralli(u : { x = two }).
+ 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 =
+ match x with
+ | Z =>
+ one
+ | S x' =>
+ two
+ end
+ in
+ (max2 z y).
+
+Define matchArgsProof
+
+:=
+ foralli(x y : nat)(u : { (matchArgs x y) = two }).
+ unjoin u with
+ end.
+
+
+Define badSub :=
+ fun(x : nat).
+ x.
+
+Define badSubTotal
+ : Forall(x:nat). Exists(y: nat). { (badSub x) = y }
+:=
+ foralli(x:nat).
+ existsi x
+ { (badSub x) = * }
+ join (badSub x) x.
+
+Total badSub badSubTotal.
+
+Define badSubProof
+ : Forall(x : nat)(x' : nat)(u : { x = (S x') }). { (badSub x) = x }
+:=
+ foralli(x : nat)(x' : nat)(u : { x = (S x') }).
+ case (badSub x) by u' ign with
+ | Z =>
+ lemma u in
+ unjoin u' contra { (badSub x) = x }
+ | S z =>
+ lemma u in
+ unjoin u' with
+ | foralli(u'' : { x = (S z) }).
+ hypjoin (badSub x) x by
+ : { x = (S z) } u''
+ : { (badSub x) = (S z) } u'
+ end
+ end
+ end.
+
+%
+% MOAR PROOOFS
+%
+%
%-
Define myproof :=
@@ -18,47 +185,86 @@
end.
-%
- %-
-Define eqnat : Fun(^ #owned n m:nat).bool :=
- fun eqnat(^ #owned 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
- -%
-
-
+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 }).
- lemma n_eq in
- unjoin u with
- | foralli(p0 : { m = Z }).
- trans : { n = Z } n_eq
- : { Z = m } symm p0
- end
+ 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 }).
- lemma n_eq in
- unjoin u with
- | foralli(m' : nat)(p3 : { m = (S m') })(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') } p3
+ : { 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 }
@@ -97,6 +303,9 @@
end
end
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}).
@@ -104,11 +313,8 @@
| ff =>
v
| tt =>
- contra
- trans : { n = m } [eqnatEq2 n m v]
- : { m != n } symm u
-
- { (eqnat n m) = ff }
+ lemma u in
+ unjoin v contra { (eqnat n m) = ff }
end.
-%
@@ -150,17 +356,15 @@
%
% This would be based on all lemmas in the lemmas set.
-%-
-Define lt_Z : Forall(a:nat).{ (lt a Z) = ff } :=
- match (lt a Z) by v ign with
+Define lt_Z2 : Forall(a:nat).{ (lt a Z) = ff } :=
+ foralli(a : nat).
+ case (lt a Z) by v ign with
| ff =>
v
| tt =>
- unjoin v with
- | contradiction =>
- end
+ unjoin v contra { (lt a Z) = ff }
end.
- -%
+
%-
Define lt_leff : Forall(a b:nat)(u:{ (lt a b) = tt }).{ (le b a) = ff }
@@ -232,7 +436,7 @@
end.
-%
-
+%-
Define minus_lt2 : Forall
(a b:nat)(u1:{ (le b a) = tt })(u2:{ (lt Z b) = tt }).{ (lt (minus a b)
a) = tt }
:=
@@ -249,163 +453,217 @@
lemma b_eq in
unjoin u1 with
%-
- | foralli(a0 : nat)(a_eq : { a = (S a0) })(p3 : { b' = Z })
- (p1 : { a0 = Z })(u : { (eqnat b' a0) = tt }).
-
- lemma
- : { (minus a b) = Z }
- hypjoin (minus a b) Z by
- : { a = (S a0) } a_eq
- : { b = (S b') } b_eq
- : { b' = Z } p3
- : { a0 = Z } p1
- end
- in
-
+ | foralli(p0 : { (lt b a) = ff })(u : { (eqnat b a) = tt }).
hypjoin (lt (minus a b) a) tt by
- : { (minus a b) = Z } ##
- : { a = (S a0) } a_eq
- : { a0 = Z } p1
+ : { b = a } [eqnatEq b a u]
+ : { (minus b b) = Z } [x_minus_x b]
+ : { b = (S b') } b_eq
end
-
-
- | foralli(a0 : nat)(p7 : { a = (S a0) })(b'0 : nat)
- (p6 : { b' = (S b'0) })(p4 : { a0 = Z })
- (u : { (eqnat b' a0) = tt }).
-
- lemma p6 p4 in
- unjoin u contra { (lt (minus a b) a) = tt }
-
-
- | foralli(a0 : nat)(p7 : { a = (S a0) })(b'0 : nat)
- (p6 : { b' = (S b'0) })(a00 : nat)(p5 : { a0 = (S a00) })
- (u : { (lt b'0 a00) = ff })(u : { (eqnat b' a0) = tt }).
-
-
-
- (a0 : nat)(p15 : { a = (S a0) })(p11 : { b' = Z })
- (a00 : nat)(p10 : { a0 = (S a00) })
-
- (a0 : nat)(p15 : { a = (S a0) })(b'0 : nat)
- (p14 : { b' = (S b'0) })(a00 : nat)
- (p13 : { a0 = (S a00) })(u : { (lt b'0 a00) = tt })
- 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 :
+ 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).
+ induction (n : nat) return
+ Forall(v: <vec A n>)(m:nat)(u: { (lt m n) = tt } )(a: A).
+ { (vec_get v m) = (vec_get (vecc a v) (S m)) }
+ with
+ | Z =>
+ foralli(v: <vec A n>)(m:nat)(u: { (lt m n) = tt } )(a: A).
+ lemma n_eq in
+ unjoin u contra { (vec_get v m) = (vec_get (vecc a v) (S m)) }
+ | S n' =>
+ foralli(v: <vec A n>)(m:nat)(u: { (lt m n) = tt } )(a: A).
+ lemma n_eq in
+ unjoin u with
+ | foralli(p2 : { m = Z }).
+ hypjoin (vec_get v m) (vec_get (vecc a v) (S m)) by
+ : { m = Z } p2
+ end
+ | foralli(m0 : nat)(p3 : { m = (S m0) })(u : { (lt m0 n') = tt }).
+ [n_IH n'
+ end
+
+
%-
- | foralli(a0 : nat)(p9 : { a = (S a0) })(u : { (eqnat b' a0) = tt }).
-
- lemma
- : { (minus a b) = (minus a' b') }
- hypjoin (minus a b) (minus a' b') by a_eq b_eq end
- in
- case b' with
- | Z =>
- lemma
- : { (minus a b) = a' }
- trans : { (minus a b) = (minus a' b') } ##
- trans : { (minus a' b') = (minus a' Z) } cong (minus a' *)
b'_eq
- : { (minus a' Z) = a' } join (minus a' Z) a'
- in
- hypjoin (lt (minus a b) a) tt by
- : { (minus a b) = a' } ##
- : { a = (S a') } a_eq
- : { (lt a' (S a')) = tt } [lt_S a']
- end
- | S b'' =>
- abbrev x = (minus a (S b')) in
- lemma
- : { (lt Z b') = tt }
- hypjoin (lt Z b') tt by b'_eq end
-
- : { (lt b' b) = tt }
- transs
- : { (lt b' b) = (lt b' (S b')) } cong (lt b' *) b_eq
- : { (lt b' (S b')) = tt } [lt_S b']
- end
-
- : { (lt b' a) = tt }
- [ltle_trans b' b a ## u1]
-
- : { (le b' a) = tt }
- [lt_implies_le b' a ##]
-
-
- : { (lt (S x) a) = tt }
- hypjoin (lt (S x) a ) tt by
- : { (minus a b') = (S x) } [minusS2 a b' ##]
- : { (lt (minus a b') a) = tt } [b_IH b' ## ##]
- end
-
- : { (lt x a) = tt }
- [lt_trans x (S x) a [lt_S x] ##]
- in
-
- hypjoin (lt (minus a b) a) tt by
- : { (lt x a) = tt } ##
- : { b = (S b') } b_eq
- end
- end
- -%
- end
- 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 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(u1:{ (le b a) = tt })(u2:{ (lt Z b) = tt }).
- contra
- trans symm b_eq
- [lt_implies_not_zero Z b u2]
-
- { (lt (minus a b) a) = tt }
- | S b' =>
- foralli(u1:{ (le b a) = tt })(u2:{ (lt Z b) = tt }).
-
- case a 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
- abbrev Z_lt_a = [ltle_trans Z b a u2 u1] in
- trans [lt_implies_not_zero Z a Z_lt_a]
- symm a_eq
-
- { (lt (minus a b) a) = tt }
- | S a' =>
- abbrev stripped =
- hypjoin (minus a b) (minus a' b') by a_eq b_eq end
+ 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
- case b' with
+ abbrev restLen_eq_n' = inj (S *) SrestLen_eq_Sn' in
+
+ case m with
| Z =>
- abbrev a_minus_b_eq_a' =
- trans stripped
- trans cong (minus a' *) b'_eq
- join (minus a' Z) a'
+ 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
- trans cong (lt * a) a_minus_b_eq_a'
- trans cong (lt a' *) a_eq
- [lt_S a']
- | S b'' =>
- abbrev z_lt_b' = hypjoin (lt Z b') tt by b'_eq end in
- abbrev b'_lt_b =
- trans cong (lt b' *) b_eq
- [lt_S b']
+ 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
- abbrev b'_lt_a = [ltle_trans b' b a b'_lt_b u1] in
- abbrev b'_le_a = [lt_implies_le b' a b'_lt_a] in
- abbrev x = (minus a (S b')) in
- abbrev Sx_lt_a =
- trans cong (lt * a)
- symm [minusS2 a b' b'_lt_a]
- [b_IH b' b'_le_a z_lt_b']
- in
- abbrev x_lt_a = [lt_trans x (S x) a [lt_S x] Sx_lt_a] in
-
- trans cong (lt * a)
- hypjoin (minus a b) x by b_eq end
- x_lt_a
- end % b'
- end % a
- end. %b
+ hypjoin (vec_get v m) (vec_last v) by
+ indStep
+ last_rest_eq_last_v
+ v_eq
+ m_eq
+ end
+ end
+ end
+ end.
+
-%
-Classify neqEqnat2.
+Classify eqnatNeq2.