feat(types.nat): prove that inequalities on nat are mere propositions

Also some small changes in various other locations
This commit is contained in:
Floris van Doorn 2015-05-23 02:32:49 -04:00 committed by Leonardo de Moura
parent 95e0fbb71a
commit c64d73aae4
10 changed files with 41 additions and 10 deletions

View file

@ -1,7 +1,6 @@
/-
Copyright (c) 2015 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn
Declaration of the interval

View file

@ -256,3 +256,6 @@ definition naive_funext_of_ua : naive_funext :=
protected definition homotopy.rec_on [recursor] {Q : (f g) → Type} (p : f g)
(H : Π(q : f = g), Q (apd10 q)) : Q p :=
right_inv apd10 p ▸ H (eq_of_homotopy p)
protected definition homotopy.rec_on_idp [recursor] {Q : Π{g}, (f g) → Type} {g : Π x, P x} (p : f g) (H : Q (homotopy.refl f)) : Q p :=
homotopy.rec_on p (λq, eq.rec_on q H)

View file

@ -1,7 +1,6 @@
/-
Copyright (c) 2015 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Floris van Doorn
Basic theorems about pathovers

View file

@ -38,13 +38,12 @@ namespace is_trunc
definition leq (n m : trunc_index) : Type₀ :=
trunc_index.rec_on n (λm, unit) (λ n p m, trunc_index.rec_on m (λ p, empty) (λ m q p, p m) p) m
notation x <= y := trunc_index.leq x y
notation x ≤ y := trunc_index.leq x y
end trunc_index
infix `+2+`:65 := trunc_index.add
notation x <= y := trunc_index.leq x y
notation x ≤ y := trunc_index.leq x y
namespace trunc_index
definition succ_le_succ {n m : trunc_index} (H : n ≤ m) : n.+1 ≤ m.+1 := H
definition le_of_succ_le_succ {n m : trunc_index} (H : n.+1 ≤ m.+1) : n ≤ m := H

View file

@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn
-/
import .basic .order .sub
import .basic .order .sub .hott

32
hott/types/nat/hott.hlean Normal file
View file

@ -0,0 +1,32 @@
/-
Copyright (c) 2015 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Floris van Doorn
Theorems about the natural numbers specific to HoTT
-/
import .basic
open is_trunc unit empty eq
namespace nat
definition is_hprop_lt [instance] (n m : ) : is_hprop (n < m) :=
begin
assert H : Π{n m : } (p : n < m) (q : succ n = m), p = q ▸ lt.base n,
{ intros, cases p,
{ assert H' : q = idp, apply is_hset.elim,
cases H', reflexivity},
{ cases q, exfalso, exact lt.irrefl b a}},
apply is_hprop.mk, intros p q,
induction q,
{ apply H},
{ cases p,
exfalso, exact lt.irrefl b a,
exact ap lt.step !v_0}
end
definition is_hprop_le (n m : ) : is_hprop (n ≤ m) := !is_hprop_lt
end nat

View file

@ -9,7 +9,7 @@ Ported from standard library
-/
import .basic algebra.ordered_ring
open core prod decidable
open prod decidable sum eq
namespace nat

View file

@ -1,7 +1,6 @@
/-
Copyright (c) 2015 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Floris van Doorn
Theorems about squareovers

View file

@ -10,7 +10,7 @@ Properties of is_trunc and trunctype
import types.pi types.eq types.equiv .function
open eq sigma sigma.ops pi function equiv is_trunc.trunctype is_equiv prod
open eq sigma sigma.ops pi function equiv is_trunc.trunctype is_equiv prod is_trunc.trunc_index
namespace is_trunc
variables {A B : Type} {n : trunc_index}

View file

@ -135,7 +135,7 @@
(,(rx (not (any "\.")) word-start
(group
(or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply"
"apply" "fapply" "eapply" "rename" "intro" "intros" "all_goals" "fold"
"apply" "fapply" "eapply" "rename" "intro" "intros" "all_goals" "fold" "focus" "focus_at"
"generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "rexact"
"refine" "repeat" "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite" "esimp"
"unfold" "change" "check_expr" "contradiction" "exfalso" "split" "existsi" "constructor" "left" "right"