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... -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/b5f593a8a3cf403ce5e026840e4c54af44... You're receiving this email because of your account on gitlab.com.