Jean-Alexandre Barszcz pushed to branch ja-barszcz at Stefan / Typer

Commits: b5f593a8 by Jean-Alexandre Barszcz at 2020-04-14T18:47:30-04:00 [WIP] proof of Decidable (a < b)

- - - - -

1 changed file:

- samples/decidable.typer

Changes:

===================================== samples/decidable.typer ===================================== @@ -113,4 +113,25 @@ decideEven =

type _<_ (a : Nat) (b : Nat) | ltZ (pa ::: Eq a zero) (pb ::: Eq b (succ ?b)) - | ltS (p : (?a < ?b)) (pa ::: Eq a (succ ?a)) (pb ::: Eq b (succ ?b)); + | ltS (p :: (?a < ?b)) (pa ::: Eq a (succ ?a)) (pb ::: Eq b (succ ?b)); + +decideLT : (a : Nat) => (b : Nat) => Decidable (a < b); +decideLT = + lambda a b => + case b + | zero => no (p := + lambda (p : (a < b)) -> + case p + | ltZ => absurd (Eq_trans b) (discriminate_nocheck zero (succ ?)) + | ltS => absurd (Eq_trans b) (discriminate_nocheck zero (succ ?))) + | succ b' => + case a + | zero => yes (p := ltZ) + | succ a' => + case (decideLT : (Decidable (a' < b'))) + | yes => yes (p := ltS) + | no => no (p := + lambda (p : (a < b)) -> + case p + | ltZ => absurd (Eq_trans a) (discriminate_nocheck zero (succ ?)) + | ltS => absurd (? : (a' < b')) (? : Not (a' < b')));

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/b5f593a8a3cf403ce5e026840e4c54af44...