HigherOrderCO/Kind1
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind1.git synced 2024-09-11 08:45:32 +03:00
Code Issues Packages Projects Releases Wiki Activity

prove ltn is preserved under multiplication by positives

Browse Source
This commit is contained in:
Rígille S. B. Menezes 2021-12-01 13:34:08 -03:00
parent ebb3436bbb
commit ddf79eeae0
3 changed files with 21 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
base/Nat/add/succ_right.kind
View File

@ -1,4 +1,4 @@
Nat.add.succ_right(a: Nat, b: Nat): (a + Nat.succ(b)) == Nat.succ(Nat.add(a,b))
Nat.add.succ_right(a: Nat, b: Nat): Equal(Nat, Nat.add(a, Nat.succ(b)), Nat.succ(Nat.add(a,b)))
case a {
zero: refl
succ:

22
base/Nat/ltn/mul.kind
View File

@ -1,8 +1,24 @@
// TODO
Nat.ltn.mul(
a: Nat
b: Nat
c: Nat
H: Equal(Bool, Nat.ltn(a, b), true)
H0: Equal(Bool, Nat.ltn(0, c), true)
H1: Equal(Bool, Nat.ltn(a, b), true)
): Equal(Bool, Nat.ltn(Nat.mul(c, a), Nat.mul(c, b)), true)
?Nat.ltn.mul
case c with H0 H1 {
succ:
let H1 = Nat.Order.mul.left(Nat.succ(a), b, Nat.succ(c.pred), H1)
let H1 = case Nat.mul.succ_right(Nat.succ(c.pred), a) {
refl:
H1
}: Equal(Bool, Nat.lte(self.b,Nat.mul(Nat.succ(c.pred),b)), true)
let H1 = H1 :: Equal(Bool, Nat.lte(Nat.succ(Nat.add(c.pred,Nat.mul(Nat.succ(c.pred),a))),Nat.mul(Nat.succ(c.pred),b)), true)
let calc = mirror(Nat.add.succ_right(c.pred, Nat.mul(Nat.succ(c.pred),a)))
let H1 = case calc {
refl:
H1
}: Equal(Bool, Nat.lte(calc.b,Nat.mul(Nat.succ(c.pred),b)), true)
Nat.lte.cut_left(c.pred, Nat.succ(Nat.mul(Nat.succ(c.pred),a)),Nat.mul(Nat.succ(c.pred),b), H1)
zero:
H0
}!

2
base/Nat/mod/mul_both.kind
View File

@ -7,7 +7,7 @@ Nat.mod.mul_both(
H1: Equal(Bool, Nat.lte(1, c), true)
): Equal(Nat, Nat.mul(a, Nat.mod(b, c)), Nat.mod(Nat.mul(a, b), Nat.mul(a, c)))
let bound_lemma = Nat.lte.comm.false(c, Nat.mod(b, c), Nat.mod.small(b, c, H1))
let bound = Nat.ltn.mul( Nat.mod(b,c), c, a, bound_lemma)
let bound = Nat.ltn.mul(Nat.mod(b,c), c, a, H0, bound_lemma)
let id_lemma = Nat.div_mod.recover(b, c, H1)
let id_lemma = apply(Nat.mul(a), id_lemma)
let distrib = Nat.mul.distrib_left(a,Nat.mod(b,c),Nat.mul(Nat.div(b,c),c))