mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-09-11 07:15:45 +03:00
prove more theorems about natural numbers
This commit is contained in:
Rígille S. B. Menezes
parent
528db93c6c
commit
1eee54b72e
155
base/Nat/AddExp.kind
Normal file
155
base/Nat/AddExp.kind
Normal file
@ -0,0 +1,155 @@
|
||||
type Nat.AddExp {
|
||||
const(value: Nat)
|
||||
var(idx: Nat)
|
||||
add(left: Nat.AddExp, right: Nat.AddExp)
|
||||
}
|
||||
|
||||
Nat.AddExp.from_nat: Nat -> Nat.AddExp
|
||||
Nat.AddExp.const
|
||||
|
||||
Nat.AddExp.dimension(
|
||||
exp: Nat.AddExp
|
||||
): Nat
|
||||
case exp {
|
||||
const:
|
||||
0
|
||||
add:
|
||||
let left_dim = Nat.AddExp.dimension(exp.left)
|
||||
let right_dim = Nat.AddExp.dimension(exp.right)
|
||||
Nat.max(left_dim, right_dim)
|
||||
var:
|
||||
Nat.succ(exp.idx)
|
||||
}
|
||||
|
||||
Nat.AddExp.constant(exp: Nat.AddExp): Type
|
||||
case exp {
|
||||
const:
|
||||
Unit
|
||||
var:
|
||||
Empty
|
||||
add:
|
||||
And<Nat.AddExp.constant(exp.left), Nat.AddExp.constant(exp.right)>
|
||||
}
|
||||
|
||||
Nat.AddExp.dimension.zero(
|
||||
exp: Nat.AddExp
|
||||
Hyp: Equal<Nat>(Nat.AddExp.dimension(exp), 0)
|
||||
): Nat.AddExp.constant(exp)
|
||||
(case exp {
|
||||
const:
|
||||
(Hyp)
|
||||
unit
|
||||
var:
|
||||
(Hyp)
|
||||
let contra = Nat.succ_neq_zero!(Hyp)
|
||||
Empty.absurd!(contra)
|
||||
add:
|
||||
(Hyp)
|
||||
let {left_small, right_small} = Nat.max.big(Nat.AddExp.dimension(exp.left), Nat.AddExp.dimension(exp.right))
|
||||
def max = Nat.max(Nat.AddExp.dimension(exp.left), Nat.AddExp.dimension(exp.right))
|
||||
let left_zero = Nat.Order.chain.aux!(Equal.rewrite<Nat>(
|
||||
max, 0, Hyp,
|
||||
(x) Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp.left), x), true),
|
||||
left_small
|
||||
))
|
||||
let right_zero = Nat.Order.chain.aux!(Equal.rewrite<Nat>(
|
||||
max, 0, Hyp
|
||||
(x) Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp.right), x), true),
|
||||
right_small
|
||||
))
|
||||
let left = Nat.AddExp.dimension.zero(exp.left, left_zero)
|
||||
let right = Nat.AddExp.dimension.zero(exp.right, right_zero)
|
||||
Pair.new!!(left, right)
|
||||
}: (Hyp: Equal<Nat>(Nat.AddExp.dimension(exp), 0)) -> Nat.AddExp.constant(exp))(
|
||||
Hyp
|
||||
)
|
||||
|
||||
Nat.AddExp.compute(
|
||||
exp: Nat.AddExp
|
||||
Hyp: Nat.AddExp.constant(exp)
|
||||
): Nat
|
||||
case exp with Hyp {
|
||||
const:
|
||||
exp.value
|
||||
var:
|
||||
Empty.absurd!(Hyp)
|
||||
add:
|
||||
open Hyp
|
||||
Nat.add(Nat.AddExp.compute(exp.left, Hyp.fst), Nat.AddExp.compute(exp.right, Hyp.snd))
|
||||
}!
|
||||
|
||||
Nat.AddExp.substitution(
|
||||
exp: Nat.AddExp
|
||||
): Variadic(Nat.AddExp.dimension(exp), Nat, Nat)
|
||||
def dim = Nat.AddExp.dimension(exp)
|
||||
def Hyp = Nat.Order.refl(dim)
|
||||
Nat.AddExp.substitution.aux0(dim, exp, Hyp)
|
||||
|
||||
Nat.AddExp.substitution.aux0(
|
||||
n: Nat
|
||||
exp: Nat.AddExp
|
||||
Hyp: Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp), n), true)
|
||||
): Variadic(n, Nat, Nat)
|
||||
case n with Hyp {
|
||||
zero:
|
||||
def Hyp = Nat.Order.chain.aux!(Hyp)
|
||||
def Hyp = Nat.AddExp.dimension.zero!(Hyp)
|
||||
Nat.AddExp.compute(exp, Hyp)
|
||||
succ:
|
||||
(value)
|
||||
def new_exp = Nat.AddExp.substitution.aux1(exp, value, n.pred)
|
||||
let Hyp = Nat.AddExp.substitution.aux2(exp, value, n.pred, Hyp)
|
||||
Nat.AddExp.substitution.aux0(n.pred, new_exp, Hyp)
|
||||
}!
|
||||
|
||||
Nat.AddExp.substitution.aux1(
|
||||
exp: Nat.AddExp
|
||||
value: Nat
|
||||
idx: Nat
|
||||
): Nat.AddExp
|
||||
case exp {
|
||||
const:
|
||||
exp
|
||||
var:
|
||||
case Nat.lte(idx, exp.idx) {
|
||||
true:
|
||||
Nat.AddExp.const(value)
|
||||
false:
|
||||
exp
|
||||
}
|
||||
add:
|
||||
Nat.AddExp.add(
|
||||
Nat.AddExp.substitution.aux1(exp.left, value, idx)
|
||||
Nat.AddExp.substitution.aux1(exp.right, value, idx)
|
||||
)
|
||||
}
|
||||
|
||||
Nat.AddExp.substitution.aux2(
|
||||
exp: Nat.AddExp
|
||||
value: Nat
|
||||
idx: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp), Nat.succ(idx)), true)
|
||||
): let new_exp = Nat.AddExp.substitution.aux1(exp, value, idx)
|
||||
Equal<Bool>(Nat.lte(Nat.AddExp.dimension(new_exp), idx), true)
|
||||
case exp with Hyp {
|
||||
const:
|
||||
Equal.refl<Bool>(true)
|
||||
var:
|
||||
def cmp = Nat.lte(idx, exp.idx)
|
||||
let cmp_eq = refl :: cmp == cmp
|
||||
case cmp with cmp_eq: ^cmp == cmp {
|
||||
true:
|
||||
Equal.refl<Bool>(true)
|
||||
false:
|
||||
Nat.lte.comm.false(idx, exp.idx, cmp_eq)
|
||||
}! :: Equal<Bool>(Nat.lte(Nat.AddExp.dimension(cmp(() Nat.AddExp, Nat.AddExp.const(value), Nat.AddExp.var(exp.idx))), idx), true)
|
||||
add:
|
||||
let {left_bound, right_bound} = Nat.max.split.left(
|
||||
Nat.AddExp.dimension(exp.left),
|
||||
Nat.AddExp.dimension(exp.right),
|
||||
Nat.succ(idx), Hyp
|
||||
)
|
||||
let ind_left = Nat.AddExp.substitution.aux2(exp.left, value, idx, left_bound)
|
||||
let ind_right = Nat.AddExp.substitution.aux2(exp.right, value, idx, right_bound)
|
||||
Nat.max.combine.left!!!(ind_left, ind_right)
|
||||
}!
|
||||
@ -2,12 +2,12 @@ Nat.lte.comm.false(
|
||||
a: Nat
|
||||
b: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(a, b), false)
|
||||
): Equal<Bool>(Nat.lte(b, a), true)
|
||||
): Equal<Bool>(Nat.lte(Nat.succ(b), a), true)
|
||||
(case a {
|
||||
zero:
|
||||
(Hyp)
|
||||
let contra = Bool.true_neq_false(Hyp)
|
||||
Empty.absurd<Equal<Bool>(Nat.lte(b, 0), true)>(contra)
|
||||
Empty.absurd<Equal<Bool>(Nat.lte(Nat.succ(b), 0), true)>(contra)
|
||||
succ:
|
||||
(Hyp)
|
||||
(case b {
|
||||
@ -18,10 +18,10 @@ Nat.lte.comm.false(
|
||||
(Hyp)
|
||||
let qed = Nat.lte.comm.false(a.pred, b.pred, Hyp)
|
||||
qed
|
||||
}: (Hyp: Equal<Bool>(Nat.lte(Nat.succ(a.pred), b), false)) -> Equal<Bool>(Nat.lte(b, Nat.succ(a.pred)), true))(
|
||||
}: (Hyp: Equal<Bool>(Nat.lte(Nat.succ(a.pred), b), false)) -> Equal<Bool>(Nat.lte(Nat.succ(b), Nat.succ(a.pred)), true))(
|
||||
Hyp
|
||||
)
|
||||
}: (Hyp: Equal<Bool>(Nat.lte(a, b), false)) -> Equal<Bool>(Nat.lte(b, a), true))(
|
||||
}: (Hyp: Equal<Bool>(Nat.lte(a, b), false)) -> Equal<Bool>(Nat.lte(Nat.succ(b), a), true))(
|
||||
Hyp
|
||||
)
|
||||
|
||||
|
||||
17
base/Nat/lte/succ_left.kind
Normal file
17
base/Nat/lte/succ_left.kind
Normal file
@ -0,0 +1,17 @@
|
||||
Nat.lte.succ_left(
|
||||
a: Nat
|
||||
b: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(Nat.succ(a), b), true)
|
||||
): Equal<Bool>(Nat.lte(a, b), true)
|
||||
case b with Hyp {
|
||||
zero:
|
||||
let contra = Bool.false_neq_true(Hyp)
|
||||
Empty.absurd!(contra)
|
||||
succ:
|
||||
case a with Hyp {
|
||||
zero:
|
||||
refl
|
||||
succ:
|
||||
Nat.lte.succ_left(a.pred, b.pred, Hyp)
|
||||
}!
|
||||
}!
|
||||
@ -11,6 +11,7 @@ Nat.max.big(
|
||||
false:
|
||||
(lemma_ab)
|
||||
let lemma_ba = Nat.lte.comm.false!!(lemma_ab)
|
||||
let lemma_ba = Nat.lte.succ_left!!(lemma_ba)
|
||||
Pair.new!!(Nat.Order.refl(a), lemma_ba)
|
||||
}: (lemma_ab: Equal<Bool>(Nat.lte(a, b), cmp_ab)) -> And<
|
||||
Equal<Bool>(Nat.lte(a, case cmp_ab { true: b, false: a }), true),
|
||||
|
||||
22
base/Nat/max/combine.kind
Normal file
22
base/Nat/max/combine.kind
Normal file
@ -0,0 +1,22 @@
|
||||
Nat.max.combine.right(
|
||||
a: Nat
|
||||
b: Nat
|
||||
c: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(a, b), true)
|
||||
): Equal<Bool>(Nat.lte(a, Nat.max(b, c)), true)
|
||||
Nat.Order.chain!!!(Hyp, Nat.max.big.left(b, c))
|
||||
|
||||
Nat.max.combine.left(
|
||||
a: Nat
|
||||
b: Nat
|
||||
c: Nat
|
||||
Hyp0: Equal<Bool>(Nat.lte(a, b), true)
|
||||
Hyp1: Equal<Bool>(Nat.lte(c, b), true)
|
||||
): Equal<Bool>(Nat.lte(Nat.max(a, c), b), true)
|
||||
def cmp_ac = Nat.lte(a, c)
|
||||
case cmp_ac {
|
||||
true:
|
||||
Hyp1
|
||||
false:
|
||||
Hyp0
|
||||
}! :: Equal<Bool>(Nat.lte(cmp_ac(() Nat, c, a), b), true)
|
||||
@ -6,6 +6,7 @@ Nat.max.comm(
|
||||
case lemma {
|
||||
fst:
|
||||
let lemma_ba = Nat.lte.comm.false!!(lemma.value)
|
||||
let lemma_ba = Nat.lte.succ_left!!(lemma_ba)
|
||||
let qed = Equal.refl<Nat>(a)
|
||||
let qed = Equal.rewrite<Bool>(
|
||||
false, Nat.lte(a, b), mirror(lemma.value),
|
||||
@ -28,6 +29,7 @@ Nat.max.comm(
|
||||
qed
|
||||
trd:
|
||||
let lemma_ab = Nat.lte.comm.false!!(lemma.value)
|
||||
let lemma_ab = Nat.lte.succ_left!!(lemma_ab)
|
||||
let qed = Equal.refl<Nat>(b)
|
||||
let qed = Equal.rewrite<Bool>(
|
||||
false, Nat.lte(b, a), mirror(lemma.value),
|
||||
|
||||
8
base/Nat/max/split.kind
Normal file
8
base/Nat/max/split.kind
Normal file
@ -0,0 +1,8 @@
|
||||
Nat.max.split.left(
|
||||
a: Nat
|
||||
b: Nat
|
||||
c: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(Nat.max(a, b), c), true)
|
||||
): And<Equal<Bool>(Nat.lte(a, c), true), Equal<Bool>(Nat.lte(b, c), true)>
|
||||
let {left_lemma, right_lemma} = Nat.max.big(a, b)
|
||||
{Nat.Order.chain!!!(left_lemma, Hyp), Nat.Order.chain!!!(right_lemma, Hyp)}
|
||||
157
base/Test.kind
157
base/Test.kind
@ -1,141 +1,16 @@
|
||||
type Nat.AddExp {
|
||||
const(value: Nat)
|
||||
var(idx: Nat)
|
||||
add(left: Nat.AddExp, right: Nat.AddExp)
|
||||
}
|
||||
|
||||
Nat.AddExp.dimension(
|
||||
exp: Nat.AddExp
|
||||
): Nat
|
||||
case exp {
|
||||
const:
|
||||
0
|
||||
add:
|
||||
let left_dim = Nat.AddExp.dimension(exp.left)
|
||||
let right_dim = Nat.AddExp.dimension(exp.right)
|
||||
Nat.max(left_dim, right_dim)
|
||||
var:
|
||||
Nat.succ(exp.idx)
|
||||
}
|
||||
|
||||
Nat.AddExp.constant(exp: Nat.AddExp): Type
|
||||
case exp {
|
||||
const:
|
||||
Unit
|
||||
var:
|
||||
Empty
|
||||
add:
|
||||
And<Nat.AddExp.constant(exp.left), Nat.AddExp.constant(exp.right)>
|
||||
}
|
||||
|
||||
Nat.AddExp.dimension.zero(
|
||||
exp: Nat.AddExp
|
||||
Hyp: Equal<Nat>(Nat.AddExp.dimension(exp), 0)
|
||||
): Nat.AddExp.constant(exp)
|
||||
(case exp {
|
||||
const:
|
||||
(Hyp)
|
||||
unit
|
||||
var:
|
||||
(Hyp)
|
||||
let contra = Nat.succ_neq_zero!(Hyp)
|
||||
Empty.absurd!(contra)
|
||||
add:
|
||||
(Hyp)
|
||||
let {left_small, right_small} = Nat.max.big(Nat.AddExp.dimension(exp.left), Nat.AddExp.dimension(exp.right))
|
||||
def max = Nat.max(Nat.AddExp.dimension(exp.left), Nat.AddExp.dimension(exp.right))
|
||||
let left_zero = Nat.Order.chain.aux!(Equal.rewrite<Nat>(
|
||||
max, 0, Hyp,
|
||||
(x) Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp.left), x), true),
|
||||
left_small
|
||||
))
|
||||
let right_zero = Nat.Order.chain.aux!(Equal.rewrite<Nat>(
|
||||
max, 0, Hyp
|
||||
(x) Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp.right), x), true),
|
||||
right_small
|
||||
))
|
||||
let left = Nat.AddExp.dimension.zero(exp.left, left_zero)
|
||||
let right = Nat.AddExp.dimension.zero(exp.right, right_zero)
|
||||
Pair.new!!(left, right)
|
||||
}: (Hyp: Equal<Nat>(Nat.AddExp.dimension(exp), 0)) -> Nat.AddExp.constant(exp))(
|
||||
Hyp
|
||||
)
|
||||
|
||||
Nat.AddExp.compute(
|
||||
exp: Nat.AddExp
|
||||
Hyp: Nat.AddExp.constant(exp)
|
||||
): Nat
|
||||
case exp with Hyp {
|
||||
const:
|
||||
exp.value
|
||||
var:
|
||||
Empty.absurd!(Hyp)
|
||||
add:
|
||||
open Hyp
|
||||
Nat.add(Nat.AddExp.compute(exp.left, Hyp.fst), Nat.AddExp.compute(exp.right, Hyp.snd))
|
||||
}!
|
||||
|
||||
Nat.AddExp.substitution(
|
||||
exp: Nat.AddExp
|
||||
): Variadic(Nat.AddExp.dimension(exp), Nat, Nat)
|
||||
def dim = Nat.AddExp.dimension(exp)
|
||||
def Hyp = Nat.Order.refl(dim)
|
||||
Nat.AddExp.substitution.aux0(dim, exp, Hyp)
|
||||
|
||||
Nat.AddExp.substitution.aux0(
|
||||
n: Nat
|
||||
exp: Nat.AddExp
|
||||
Hyp: Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp), n), true)
|
||||
): Variadic(n, Nat, Nat)
|
||||
case n with Hyp {
|
||||
zero:
|
||||
def Hyp = Nat.Order.chain.aux!(Hyp)
|
||||
def Hyp = Nat.AddExp.dimension.zero!(Hyp)
|
||||
Nat.AddExp.compute(exp, Hyp)
|
||||
succ:
|
||||
(value)
|
||||
def new_exp = Nat.AddExp.substitution.aux1(exp, value, Nat.succ(n.pred))
|
||||
let Hyp = Nat.AddExp.substitution.aux2(exp, value, Nat.succ(n.pred), Hyp)
|
||||
Nat.AddExp.substitution.aux0(n.pred, new_exp, Hyp)
|
||||
}!
|
||||
|
||||
Nat.AddExp.substitution.aux1(
|
||||
exp: Nat.AddExp
|
||||
value: Nat
|
||||
idx: Nat
|
||||
): Nat.AddExp
|
||||
case exp {
|
||||
const:
|
||||
exp
|
||||
var:
|
||||
case Nat.lte(idx, exp.idx) {
|
||||
true:
|
||||
Nat.AddExp.const(value)
|
||||
false:
|
||||
exp
|
||||
}
|
||||
add:
|
||||
Nat.AddExp.add(
|
||||
Nat.AddExp.substitution.aux1(exp.left, value, idx)
|
||||
Nat.AddExp.substitution.aux1(exp.right, value, idx)
|
||||
)
|
||||
}
|
||||
|
||||
Nat.AddExp.substitution.aux2(
|
||||
exp: Nat.AddExp
|
||||
value: Nat
|
||||
idx: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp), idx), true)
|
||||
): let new_exp = Nat.AddExp.substitution.aux1(exp, value, idx)
|
||||
Equal<Bool>(Nat.lte(Nat.AddExp.dimension(new_exp), Nat.pred(idx)), true)
|
||||
case exp with Hyp {
|
||||
const:
|
||||
Equal.refl<Bool>(true)
|
||||
var:
|
||||
?var
|
||||
add:
|
||||
?add
|
||||
}!
|
||||
|
||||
Test: _
|
||||
"hi"
|
||||
Test<A: Type, B: Type>(
|
||||
f: A -> B,
|
||||
Hyp: (
|
||||
C: Type
|
||||
g: B -> C
|
||||
h: B -> C
|
||||
a: A
|
||||
HHyp: g(f(a)) == h(f(a))
|
||||
b: B
|
||||
) -> g(b) == h(b)
|
||||
target: B
|
||||
): [a: A] f(a) == target
|
||||
let g = ((b) true) :: B -> Bool
|
||||
let h = ((b) Decidable([a: A] f(a) == b)) :: B -> Bool
|
||||
let hmm = Hyp(Type, g, h)
|
||||
?test
|
||||
|
||||
Loading…
Reference in New Issue
Block a user