[guru-lang] r544 committed - fixed some issues with unjoin. added unjoin contradictions.
guru...@googlecode.com
Author: kevinclancy0
Date: Fri Oct 21 12:38:46 2011
Log: fixed some issues with unjoin. added unjoin contradictions.
http://code.google.com/p/guru-lang/source/detail?r=544
Modified:
/branches/1.0/guru/Expr.java
/branches/1.0/guru/Match.java
/branches/1.0/guru/Parser.java
/branches/1.0/guru/Unjoin.java
/branches/1.0/guru/UnjoinContext.java
/branches/1.0/guru/UnjoinDeduction.java
/branches/1.0/tests/unjoin.g
=======================================
--- /branches/1.0/guru/Expr.java Wed Oct 12 12:15:28 2011
+++ /branches/1.0/guru/Expr.java Fri Oct 21 12:38:46 2011
@@ -108,6 +108,7 @@
public static final int LEMMA_MARK = 91;
public static final int ASCRIPTION = 92;
public static final int UNJOIN = 93;
+ public static final int UNJOIN_CONTRA = 94;
public static final int LAST = 200;
=======================================
--- /branches/1.0/guru/Match.java Wed Oct 12 12:15:28 2011
+++ /branches/1.0/guru/Match.java Fri Oct 21 12:38:46 2011
@@ -182,6 +182,7 @@
for(int i = 0; i < C.length; ++i)
{
Case c = C[i];
+ UnjoinDeduction scrutDeduction = UnjoinDeduction.empty;
if (t_.construct == TERM_APP)
{
@@ -195,12 +196,35 @@
if (t_ != c.c)
continue;
}
+ else if (t_.construct == MATCH)
+ {
+ if(c.x.length == 0)
+ {
+ scrutDeduction = t_.Unjoin(
+ c.c,
+ uCtxt,
+ baseCtxt,
+ true
+ );
+ }
+ else
+ {
+ scrutDeduction = t_.Unjoin(
+ new TermApp(c.c,c.x),
+ uCtxt,
+ baseCtxt,
+ true
+ );
+ }
+ }
// Prepend immediate deductions onto case body deductions -----
if (c.x.length == 0)
{
// Make deductions from case body -----
- branch = c.body.Unjoin(
+ branch = UnjoinDeduction.FancyAppend(
+ UnjoinDeduction.Simplify(scrutDeduction),
+ c.body,
target,
uCtxt,
baseCtxt,
@@ -217,78 +241,82 @@
else
{
FunType consType =
(FunType)c.c.classify(baseCtxt).defExpandTop(baseCtxt);
-
- // Create contstructor argument variable -----
- Var[] clones = new Var[c.x.length];
- Expr[] types = new Expr[c.x.length];
-
+
// A version of body for which variables corresponding to
// match arguments are replaced with their corresponding
// unjoin introductions.
Expr body = c.body;
-
- int last = c.x.length-1;
- for(int j = 0; j <= last; ++j)
- {
-
- clones[j] = new Var(uCtxt.genName(c.x[j].name));
- types[j] = consType.types[0];
-
- //TODO: This seems a bit inefficient. Could we optimize this?
- body = body.subst(clones[j], c.x[j]);
-
- // 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]);
- }
-
- // Make deductions from case body -----
- branch = body.Unjoin(
- target,
- uCtxt,
- baseCtxt,
- eq
- );
-
- for(int j = 0; j < c.x.length; ++j)
- uCtxt.removeName(clones[j].name);
-
- //prepend immediate deductions to case body deductions
- if(t_.construct == VAR)
- {
- // Create match proof (i.e. { scrutinee = match case } ) -----
- Atom matchEq = new Atom(true, t, new TermApp(c.c,clones));
- Var matchEqVar = new Var("p" + Integer.toString(varNum++));
- branch = new UnjoinIntro(matchEqVar, matchEq, branch);
- }
- else if (t_.construct == TERM_APP)
- {
- TermApp ta = (TermApp)t_;
-
+ // Create contstructor argument variable -----
+
+
+ if (t_.construct == TERM_APP)
+ {
+ TermApp ta = (TermApp)t_;
+ Expr substitutedBody = body;
+
for (int j = 0; j < ta.X.length; ++j)
- {
- Atom varEq = new Atom(true, ta.X[j], clones[j]);
- Var varEqProof = new Var("p" + Integer.toString(varNum++));
- branch = new UnjoinIntro(varEqProof, varEq, branch);
- }
- }
-
- for (int j = c.x.length-1; j >= 0; --j)
- branch = new UnjoinIntro(clones[j], types[j], branch);
- }
-
- if (t_.construct == MATCH)
- {
- UnjoinDeduction tDeduction = t_.Unjoin(
- new TermApp(c.c,c.x),
- uCtxt,
- baseCtxt,
- true
- );
-
- branch = UnjoinDeduction.Append(branch, tDeduction);
- }
+ substitutedBody = substitutedBody.subst(ta.X[j], c.x[j]);
+
+ branch = substitutedBody.Unjoin(
+ target,
+ uCtxt,
+ baseCtxt,
+ eq
+ );
+ }
+ else
+ {
+
+ Var[] clones = new Var[c.x.length];
+ Expr[] types = new Expr[c.x.length];
+ int last = c.x.length-1;
+
+ String prefix = ((Var)t_).name;
+
+ for(int j = 0; j <= last; ++j)
+ {
+ clones[j] = new Var(uCtxt.genName(prefix + String.valueOf(j)));
+ types[j] = consType.types[j];
+
+ //TODO: This seems a bit inefficient. Could we optimize this?
+ body = body.subst(clones[j], c.x[j]);
+
+ // 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]);
+ }
+
+ // Make deductions from case body -----
+ branch = UnjoinDeduction.FancyAppend(
+ UnjoinDeduction.Simplify(scrutDeduction),
+ body,
+ target,
+ uCtxt,
+ baseCtxt,
+ eq
+ );
+
+
+ //prepend immediate deductions to case body deductions
+ //could this be anything other than a var?
+ if(t_.construct == VAR)
+ {
+ // Create match proof (i.e. { scrutinee = match case } ) -----
+ Atom matchEq = new Atom(true, t_, new TermApp(c.c,clones));
+ Var matchEqVar = new Var("p" + Integer.toString(varNum++));
+ branch = new UnjoinIntro(matchEqVar, matchEq, branch);
+ }
+
+ for (int j = c.x.length-1; j >= 0; --j)
+ branch = new UnjoinIntro(clones[j], types[j], branch);
+
+
+ for(int j = 0; j < c.x.length; ++j)
+ uCtxt.removeName(clones[j].name);
+ }
+
+ }
//Or the current return value with the deduction for the
//current branch (if ret is null, we set it to the current branch)
=======================================
--- /branches/1.0/guru/Parser.java Wed Oct 12 12:15:28 2011
+++ /branches/1.0/guru/Parser.java Fri Oct 21 12:38:46 2011
@@ -452,7 +452,7 @@
}
- protected Unjoin readUnjoin() throws IOException
+ protected Expr readUnjoin() throws IOException
{
if (!eat_ws())
handleError("Unexpected end of input parsing an unjoin proof.");
@@ -462,31 +462,39 @@
if (!eat_ws())
handleError("Unexpected end of input parsing an unjoin proof.");
- eat("by", "unjoin proof");
-
- if (!eat_ws())
- handleError("Unexpected end of input parsing an unjoin proof.");
-
- //TODO: read some lemmas and add them into the lemma set using
- //lemma AST nodes.
-
- eat("with", "unjoin proof");
-
- if (!eat_ws())
- handleError("Unexpected end of input parsing an unjoin proof.");
-
- Vector paths = new Vector();
- while (tryToEat("|"))
- {
- paths.add(readProof());
+
+ if( tryToEat("contra") )
+ {
+ // read contra unjoin
if (!eat_ws())
handleError("Unexpected end of input parsing an unjoin
proof.");
- }
-
- eat("end", "unjoin proof");
-
- return new Unjoin(scrutinee, paths);
+
+ Expr conclusion = readFormula();
+
+ return new UnjoinContra(scrutinee, conclusion);
+ }
+ else
+ {
+ // read non-contra unjoin
+ eat("with", "unjoin proof");
+
+ if (!eat_ws())
+ handleError("Unexpected end of input parsing an unjoin
proof.");
+
+ Vector paths = new Vector();
+ while (tryToEat("|"))
+ {
+ paths.add(readProof());
+
+ if (!eat_ws())
+ handleError("Unexpected end of input parsing an unjoin
proof.");
+ }
+
+ eat("end", "unjoin proof");
+
+ return new Unjoin(scrutinee, paths);
+ }
}
protected Set readSet() throws IOException
=======================================
--- /branches/1.0/guru/Unjoin.java Wed Oct 12 12:15:28 2011
+++ /branches/1.0/guru/Unjoin.java Fri Oct 21 12:38:46 2011
@@ -67,10 +67,10 @@
}
UnjoinDeduction deduction = scrutinee.Y1.Unjoin(
- scrutinee.Y2,
- new UnjoinContext(ctxt),
- ctxt,
- scrutinee.equality
+ scrutinee.Y2,
+ new UnjoinContext(ctxt),
+ ctxt,
+ scrutinee.equality
);
=======================================
--- /branches/1.0/guru/UnjoinContext.java Wed Oct 12 12:15:28 2011
+++ /branches/1.0/guru/UnjoinContext.java Fri Oct 21 12:38:46 2011
@@ -79,12 +79,10 @@
String currentCandidate = suggestion;
boolean alreadyUsed = varNames.contains(currentCandidate);
- alreadyUsed |= (baseContext.lookup(currentCandidate) != null);
while (alreadyUsed) {
currentCandidate += "'";
alreadyUsed = varNames.contains(currentCandidate);
- alreadyUsed |= (baseContext.lookup(currentCandidate) != null);
}
varNames.add(currentCandidate);
=======================================
--- /branches/1.0/guru/UnjoinDeduction.java Wed Oct 12 12:15:28 2011
+++ /branches/1.0/guru/UnjoinDeduction.java Fri Oct 21 12:38:46 2011
@@ -13,6 +13,112 @@
public static final UnjoinDeduction empty = new UnjoinEmpty();
abstract public int GetDeductionType();
+
+ static public UnjoinDeduction Simplify(UnjoinDeduction target)
+ {
+ switch (target.GetDeductionType())
+ {
+ case INTRO:
+ UnjoinIntro intro = (UnjoinIntro)target;
+ UnjoinDeduction rest = Simplify(intro.rest);
+ if (rest == contradiction)
+ return contradiction;
+ else
+ return new UnjoinIntro(
+ intro.introVar,
+ intro.introVarType,
+ rest
+ );
+ case OR:
+ UnjoinOr or = (UnjoinOr)target;
+ if (or.d0 == contradiction && or.d1 == contradiction)
+ return contradiction;
+ else if (or.d0 == contradiction)
+ return or.d1;
+ else if (or.d1 == contradiction)
+ return or.d0;
+ else
+ return or;
+ case CONTRADICTION:
+ return contradiction;
+ case EMPTY:
+ return empty;
+ }
+
+ assert(false);
+ return null;
+ }
+
+ static public UnjoinDeduction FancyAppend(
+ UnjoinDeduction baseDeduction,
+ Expr startTerm,
+ Expr target,
+ UnjoinContext uCtxt,
+ Context baseCtxt,
+ boolean eq
+ )
+ {
+ switch (baseDeduction.GetDeductionType())
+ {
+ case INTRO:
+ UnjoinIntro intro = (UnjoinIntro)baseDeduction;
+
+ //okay... basically, I need to collapse contradictory
+ //paths, as I was originally planning to do, so that
+ //I can add everything to the context here.
+ if (intro.introVarType.construct == Expr.ATOM)
+ uCtxt.lemmaSet.addLemma(intro.introVarType);
+ else if (intro.introVarType.isTypeOrKind(baseCtxt))
+ baseCtxt.setClassifier(intro.introVar, intro.introVarType);
+
+ UnjoinDeduction ret = new UnjoinIntro(
+ intro.introVar,
+ intro.introVarType,
+ FancyAppend(
+ intro.rest,
+ startTerm,
+ target,
+ uCtxt,
+ baseCtxt,
+ eq
+ )
+ );
+
+ if (intro.introVarType.construct == Expr.ATOM)
+ uCtxt.lemmaSet.removeLemma(intro.introVarType);
+
+ return ret;
+ case OR:
+ UnjoinOr or = (UnjoinOr)baseDeduction;
+
+ UnjoinDeduction d0 = FancyAppend(
+ or.d0,
+ startTerm,
+ target,
+ uCtxt,
+ baseCtxt,
+ eq
+ );
+
+ UnjoinDeduction d1 = FancyAppend(
+ or.d1,
+ startTerm,
+ target,
+ uCtxt,
+ baseCtxt,
+ eq
+ );
+
+ return new UnjoinOr(d0, d1);
+ case CONTRADICTION:
+ return contradiction;
+ case EMPTY:
+ return startTerm.Unjoin(target, uCtxt, baseCtxt, eq);
+ }
+
+ assert(false);
+ return null;
+ }
static public UnjoinDeduction Append(
UnjoinDeduction appendThis,
@@ -22,7 +128,12 @@
switch (ontoThis.GetDeductionType())
{
case INTRO:
- return Append(appendThis, ((UnjoinIntro)ontoThis).rest);
+ UnjoinIntro intro = (UnjoinIntro)ontoThis;
+ return new UnjoinIntro(
+ intro.introVar,
+ intro.introVarType,
+ Append(appendThis, ((UnjoinIntro)ontoThis).rest)
+ );
case OR:
UnjoinOr or = (UnjoinOr)ontoThis;
return new UnjoinOr(Append(appendThis, or.d0), Append(appendThis,
or.d1));
=======================================
--- /branches/1.0/tests/unjoin.g Wed Oct 12 13:04:29 2011
+++ /branches/1.0/tests/unjoin.g Fri Oct 21 12:38:46 2011
@@ -2,11 +2,12 @@
Include "../lib/nat.g"
Include "../lib/bool.g"
Include "../lib/minus.g"
+Include "../lib/vec.g"
%-
Define myproof :=
foralli(a b : nat)(x:{ (lt a b) = tt } ).
- unjoin x by with
+ 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
@@ -31,37 +32,206 @@
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 by with
- | foralli(p0 : { m = Z }).
- trans : { n = Z } n_eq
- : { Z = m } symm p0
- end
- | S z' =>
- foralli(m: nat)(u : { (eqnat n m) = tt }).
- lemma n_eq in
- unjoin u by with
- | foralli(n' : nat)(p4 : { z' = n' })(m' : nat)(p3 : { m = (S m') })
- (u : { (eqnat n' m') = tt }).
- lemma
- : { (eqnat z' m') = tt }
- trans : { (eqnat z' m') = (eqnat n' m') } cong (eqnat * m') p4
- : { (eqnat n' m') = tt } u
- in
-
- hypjoin n m by
- : { z' = m' } [n_IH z' m' ##]
- : { m = (S m') } p3
- : { n = (S z') } n_eq
- end
+ | 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
+ | 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 }).
+ hypjoin n m by
+ : { n' = m' } [n_IH n' m' u]
+ : { m = (S m') } p3
+ : { n = (S n') } n_eq
end
+ end
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 }
+ with
+ | Z =>
+ foralli(m:nat)(u:{(eqnat n m) = ff}).
+ lemma n_eq in
+ unjoin u with
+ | foralli(m' : nat)(p5 : { m = (S m') }).
+ transs
+ : { n = Z } n_eq
+ : { Z != (S m') } clash Z (S m')
+ : { (S m') = m } symm p5
+ end
+ end
+ | S n' =>
+ foralli(m:nat)(u:{(eqnat n m) = ff}).
+ lemma n_eq in
+ unjoin u with
+ | foralli(p6 : { m = Z }).
+ transs
+ : { n = (S n') } n_eq
+ : { (S n') != Z } clash (S n') Z
+ : { Z = m } symm p6
+ end
+ | foralli(m' : nat)(p7 : { m = (S m') })(u : { (eqnat n' m') = ff }).
+ lemma
+ : { (S n') != (S m') }
+ ncong (S *) (S n') (S m')
+ : { n' != m' } [n_IH n' m' u]
+ in
+ transs
+ : { n = (S n') } n_eq
+ : { (S n') != (S m') } ##
+ : { (S m') = m } symm p7
+ end
+ end
+ end
+
+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 =>
+ contra
+ trans : { n = m } [eqnatEq2 n m v]
+ : { m != n } symm u
+
+ { (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.
+
+Define eqnat_refl2 : Forall(x:nat).{ (eqnat x x) = tt } :=
+ foralli(x:nat).
+ case (eqnat x x) by u ign with
+ | ff =>
+ unjoin u by
+
+ end
+ | tt =>
+ end
+-%
+
+% eqnat_symm - unjoin wouldn't help here
+
+% Sneq_neq2 - unjoin wouldn't help here
+
+% x_lt_x - wouldn't help
+
+% x_eqnat_x - wouldn't help
+
+% eqEqnat - wouldn't help
+
+% x_le_x - wouldn't help
+
+% leZ - wouldn't help
+
+% unjoin should be symmetric - don't give any lemma special status. instead
+% keep track of unjoined lemmas, and systematically unjoin all lemmas
recursively.
+%
+% unjoin with
+% |
+% |
+% end.
+%
+% 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
+ | ff =>
+ v
+ | tt =>
+ unjoin v with
+ | contradiction =>
+ end
+ 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 -%
+
+%-
+Define lt_lt_impliesEq2: Forall(x y:nat)(u: {(lt x y) = ff})(v:{(lt y x) =
ff}).{x = y} :=
+ induction(x:nat) return
+ Forall(y:nat)(u: {(lt x y) = ff})(v:{(lt y x) = ff}).{x = y}
+ with
+ | Z =>
+ foralli(y:nat)(u: {(lt x y) = ff})(v:{(lt y x) = ff}).
+ lemma x_eq in
+ unjoin u with
+ | foralli(p8 : { y = Z }).
+ trans : { x = Z } x_eq
+ : { Z = y } symm p8
+ end
+ | S x' =>
+ foralli(y:nat)(u: {(lt x y) = ff})(v:{(lt y x) = ff}).
+ lemma x_eq in
+ unjoin u with
+ | foralli(p10 : { y = Z }).
+ lemma p10 in
+ unjoin v with
+
+ | foralli(b' : nat)(p11 : { y = (S b') })(u : { (lt x' b') = ff }).
+
+ end
+ end.
+-%
+
+
+%-
+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 }
@@ -70,74 +240,115 @@
induction (b:nat) return
Forall(u1:{ (le b a) = tt })(u2:{ (lt Z b) = tt }).{ (lt (minus a b)
a) = tt }
with
-
- %- Z =>
- unjoin u2 by b_eq proving Forall(u1:{ (le b a) = tt })(u2:{ (lt Z
b) = tt }).{ (lt (minus a b) a) = tt }
- | S b' => ...
-
- -%
-
- | default nat =>
- foralli(u1:{ (le b a) = tt })(u2:{ (lt Z b) = tt }).
- unjoin u2 by with
- | foralli(b' : nat)(b_eq : { b = (S b') }).
- lemma b_eq in
- unjoin u1 by with
- | foralli(n' : nat)(a' : nat)(a_eq : { a = (S a') })(u : { (eqnat
n' a') = 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 ##]
+ | 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(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
+
+ hypjoin (lt (minus a b) a) tt by
+ : { (minus a b) = Z } ##
+ : { a = (S a0) } a_eq
+ : { a0 = Z } p1
+ 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(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
+ : { (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
- end.
+ end.
%-
@@ -197,4 +408,4 @@
end. %b
-%
-Classify eqnatEq.
+Classify neqEqnat2.