refactor(library/standard): integrate hott with standard library
This commit is contained in:
Jeremy Avigad
Leonardo de Moura
parent
218c9dfc81
commit
7d7655c3f1
29 changed files with 291 additions and 554 deletions
|
|
@ -1,32 +0,0 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura
|
||||
import logic bool
|
||||
using logic
|
||||
|
||||
inductive inhabited (A : Type) : Type :=
|
||||
| inhabited_intro : A → inhabited A
|
||||
|
||||
theorem inhabited_elim {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B
|
||||
:= inhabited_rec H2 H1
|
||||
|
||||
theorem inhabited_fun [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B)
|
||||
:= inhabited_elim H (take (b : B), inhabited_intro (λ a : A, b))
|
||||
|
||||
theorem inhabited_sum_left [instance] {A : Type} (B : Type) (H : inhabited A) : inhabited (A + B)
|
||||
:= inhabited_elim H (λ a, inhabited_intro (inl B a))
|
||||
|
||||
theorem inhabited_sum_right [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A + B)
|
||||
:= inhabited_elim H (λ b, inhabited_intro (inr A b))
|
||||
|
||||
theorem inhabited_product [instance] {A : Type} {B : Type} (Ha : inhabited A) (Hb : inhabited B) : inhabited (A × B)
|
||||
:= inhabited_elim Ha (λ a, (inhabited_elim Hb (λ b, inhabited_intro (a, b))))
|
||||
|
||||
theorem inhabited_bool [instance] : inhabited bool
|
||||
:= inhabited_intro true
|
||||
|
||||
theorem inhabited_unit [instance] : inhabited unit
|
||||
:= inhabited_intro ⋆
|
||||
|
||||
theorem inhabited_sigma_pr1 {A : Type} {B : A → Type} (p : Σ x, B x) : inhabited A
|
||||
:= inhabited_intro (dpr1 p)
|
||||
|
|
@ -1,343 +0,0 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura, Jeremy Avigad
|
||||
-- Ported from Coq HoTT
|
||||
|
||||
notation `assume` binders `,` r:(scoped f, f) := r
|
||||
notation `take` binders `,` r:(scoped f, f) := r
|
||||
|
||||
abbreviation id {A : Type} (a : A) := a
|
||||
abbreviation compose {A : Type} {B : Type} {C : Type} (g : B → C) (f : A → B) := λ x, g (f x)
|
||||
infixl `∘`:60 := compose
|
||||
|
||||
|
||||
-- -- Equivalences
|
||||
-- -- ------------
|
||||
|
||||
-- abbreviation Sect {A B : Type} (s : A → B) (r : B → A) := Πx : A, r (s x) ≈ x
|
||||
|
||||
-- -- TODO: need better means of declaring structures
|
||||
-- -- TODO: note that Coq allows projections to be declared to be coercions on the fly
|
||||
-- -- TODO: also think about namespaces: what should be in / out?
|
||||
-- -- TODO: can we omit ': Type'?
|
||||
|
||||
-- -- Structure IsEquiv
|
||||
|
||||
-- inductive IsEquiv {A B : Type} (f : A → B) : Type :=
|
||||
-- | IsEquiv_mk : Π
|
||||
-- (equiv_inv : B → A)
|
||||
-- (eisretr : Sect equiv_inv f)
|
||||
-- (eissect : Sect f equiv_inv)
|
||||
-- (eisadj : Πx, eisretr (f x) ≈ ap f (eissect x)),
|
||||
-- IsEquiv f
|
||||
|
||||
-- definition equiv_inv {A B : Type} {f : A → B} (H : IsEquiv f) : B → A :=
|
||||
-- IsEquiv_rec (λequiv_inv eisretr eissect eisadj, equiv_inv) H
|
||||
|
||||
-- -- TODO: note: does not type check without giving the type
|
||||
-- definition eisretr {A B : Type} {f : A → B} (H : IsEquiv f) : Sect (equiv_inv H) f :=
|
||||
-- IsEquiv_rec (λequiv_inv eisretr eissect eisadj, eisretr) H
|
||||
|
||||
-- definition eissect {A B : Type} {f : A → B} (H : IsEquiv f) : Sect f (equiv_inv H) :=
|
||||
-- IsEquiv_rec (λequiv_inv eisretr eissect eisadj, eissect) H
|
||||
|
||||
-- definition eisadj {A B : Type} {f : A → B} (H : IsEquiv f) :
|
||||
-- Πx, eisretr H (f x) ≈ ap f (eissect H x) :=
|
||||
-- IsEquiv_rec (λequiv_inv eisretr eissect eisadj, eisadj) H
|
||||
|
||||
-- -- Structure Equiv
|
||||
|
||||
-- inductive Equiv (A B : Type) : Type :=
|
||||
-- | Equiv_mk : Π
|
||||
-- (equiv_fun : A → B)
|
||||
-- (equiv_isequiv : IsEquiv equiv_fun),
|
||||
-- Equiv A B
|
||||
|
||||
-- definition equiv_fun {A B : Type} (e : Equiv A B) : A → B :=
|
||||
-- Equiv_rec (λequiv_fun equiv_isequiv, equiv_fun) e
|
||||
|
||||
-- -- TODO: use a type class instead?
|
||||
-- coercion equiv_fun : Equiv
|
||||
|
||||
-- definition equiv_isequiv [coercion] {A B : Type} (e : Equiv A B) : IsEquiv (equiv_fun e) :=
|
||||
-- Equiv_rec (λequiv_fun equiv_isequiv, equiv_isequiv) e
|
||||
|
||||
-- -- coercion equiv_isequiv
|
||||
|
||||
-- -- TODO: better symbol
|
||||
-- infix `<~>`:25 := Equiv
|
||||
-- notation e `⁻¹`:75 := equiv_inv e
|
||||
|
||||
|
||||
-- -- Truncation levels
|
||||
-- -- -----------------
|
||||
|
||||
-- inductive Contr (A : Type) : Type :=
|
||||
-- | Contr_mk : Π
|
||||
-- (center : A)
|
||||
-- (contr : Πy : A, center ≈ y),
|
||||
-- Contr A
|
||||
|
||||
-- definition center {A : Type} (C : Contr A) : A := Contr_rec (λcenter contr, center) C
|
||||
|
||||
-- definition contr {A : Type} (C : Contr A) : Πy : A, center C ≈ y :=
|
||||
-- Contr_rec (λcenter contr, contr) C
|
||||
|
||||
-- inductive trunc_index : Type :=
|
||||
-- | minus_two : trunc_index
|
||||
-- | trunc_S : trunc_index → trunc_index
|
||||
|
||||
-- -- TODO: add coercions to / from nat
|
||||
|
||||
-- -- TODO: note in the Coq version, there is an internal version
|
||||
-- definition IsTrunc (n : trunc_index) : Type → Type :=
|
||||
-- trunc_index_rec (λA, Contr A) (λn trunc_n A, (Π(x y : A), trunc_n (x ≈ y))) n
|
||||
|
||||
-- -- TODO: in the Coq version, this is notation
|
||||
-- abbreviation minus_one := trunc_S minus_two
|
||||
-- abbreviation IsHProp := IsTrunc minus_one
|
||||
-- abbreviation IsHSet := IsTrunc (trunc_S minus_one)
|
||||
|
||||
-- prefix `!`:75 := center
|
||||
|
||||
|
||||
-- -- Funext
|
||||
-- -- ------
|
||||
|
||||
-- -- TODO: move this to an "axioms" folder
|
||||
-- -- TODO: take a look at the Coq tricks
|
||||
-- axiom funext {A : Type} {P : A → Type} (f g : Π x : A, P x) : IsEquiv (@apD10 A P f g)
|
||||
|
||||
-- definition path_forall {A : Type} {P : A → Type} (f g : Π x : A, P x) : f ∼ g → f ≈ g :=
|
||||
-- (funext f g)⁻¹
|
||||
|
||||
-- definition path_forall2 {A B : Type} {P : A → B → Type} (f g : Π x y, P x y) :
|
||||
-- (Πx y, f x y ≈ g x y) → f ≈ g :=
|
||||
-- λE, path_forall f g (λx, path_forall (f x) (g x) (E x))
|
||||
|
||||
|
||||
-- -- Empty type
|
||||
-- -- ----------
|
||||
|
||||
-- inductive empty : Type
|
||||
|
||||
-- theorem empty_elim (A : Type) (H : empty) : A :=
|
||||
-- empty_rec (λ e, A) H
|
||||
|
||||
|
||||
|
||||
|
||||
-- inductive true : Prop :=
|
||||
-- | trivial : true
|
||||
|
||||
-- abbreviation not (a : Prop) := a → false
|
||||
-- prefix `¬`:40 := not
|
||||
|
||||
|
||||
|
||||
-- theorem trans_refl_right {A : Type} {x y : A} (p : x = y) : p = p ⬝ (refl y)
|
||||
-- := refl p
|
||||
|
||||
-- theorem trans_refl_left {A : Type} {x y : A} (p : x = y) : p = (refl x) ⬝ p
|
||||
-- := path_rec (trans_refl_right (refl x)) p
|
||||
|
||||
-- theorem refl_symm {A : Type} (x : A) : (refl x)⁻¹ = (refl x)
|
||||
-- := refl (refl x)
|
||||
|
||||
-- theorem refl_trans {A : Type} (x : A) : (refl x) ⬝ (refl x) = (refl x)
|
||||
-- := refl (refl x)
|
||||
|
||||
-- theorem trans_symm {A : Type} {x y : A} (p : x = y) : p ⬝ p⁻¹ = refl x
|
||||
-- := have q : (refl x) ⬝ (refl x)⁻¹ = refl x, from
|
||||
-- ((refl_symm x)⁻¹)*(refl_trans x),
|
||||
-- path_rec q p
|
||||
|
||||
-- theorem symm_trans {A : Type} {x y : A} (p : x = y) : p⁻¹ ⬝ p = refl y
|
||||
-- := have q : (refl x)⁻¹ ⬝ (refl x) = refl x, from
|
||||
-- ((refl_symm x)⁻¹)*(refl_trans x),
|
||||
-- path_rec q p
|
||||
|
||||
-- theorem symm_symm {A : Type} {x y : A} (p : x = y) : (p⁻¹)⁻¹ = p
|
||||
-- := have q : ((refl x)⁻¹)⁻¹ = refl x, from
|
||||
-- refl (refl x),
|
||||
-- path_rec q p
|
||||
|
||||
-- theorem trans_assoc {A : Type} {x y z w : A} (p : x = y) (q : y = z) (r : z = w) : p ⬝ (q ⬝ r) = (p ⬝ q) ⬝ r
|
||||
-- := have e1 : (p ⬝ q) ⬝ (refl z) = p ⬝ q, from
|
||||
-- (trans_refl_right (p ⬝ q))⁻¹,
|
||||
-- have e2 : q ⬝ (refl z) = q, from
|
||||
-- (trans_refl_right q)⁻¹,
|
||||
-- have e3 : p ⬝ (q ⬝ (refl z)) = p ⬝ q, from
|
||||
-- e2*(refl (p ⬝ (q ⬝ (refl z)))),
|
||||
-- path_rec (e3 ⬝ e1⁻¹) r
|
||||
|
||||
-- definition ap {A : Type} {B : Type} (f : A → B) {a b : A} (p : a = b) : f a = f b
|
||||
-- := p*(refl (f a))
|
||||
|
||||
-- theorem ap_refl {A : Type} {B : Type} (f : A → B) (a : A) : ap f (refl a) = refl (f a)
|
||||
-- := refl (refl (f a))
|
||||
|
||||
-- section
|
||||
-- parameters {A : Type} {B : Type} {C : Type}
|
||||
-- parameters (f : A → B) (g : B → C)
|
||||
-- parameters (x y z : A) (p : x = y) (q : y = z)
|
||||
|
||||
-- theorem ap_trans_dist : ap f (p ⬝ q) = (ap f p) ⬝ (ap f q)
|
||||
-- := have e1 : ap f (p ⬝ refl y) = (ap f p) ⬝ (ap f (refl y)), from refl _,
|
||||
-- path_rec e1 q
|
||||
|
||||
-- theorem ap_inv_dist : ap f (p⁻¹) = (ap f p)⁻¹
|
||||
-- := have e1 : ap f ((refl x)⁻¹) = (ap f (refl x))⁻¹, from refl _,
|
||||
-- path_rec e1 p
|
||||
|
||||
-- theorem ap_compose : ap g (ap f p) = ap (g∘f) p
|
||||
-- := have e1 : ap g (ap f (refl x)) = ap (g∘f) (refl x), from refl _,
|
||||
-- path_rec e1 p
|
||||
|
||||
-- theorem ap_id : ap id p = p
|
||||
-- := have e1 : ap id (refl x) = (refl x), from refl (refl x),
|
||||
-- path_rec e1 p
|
||||
-- end
|
||||
|
||||
-- section
|
||||
-- parameters {A : Type} {B : A → Type} (f : Π x, B x)
|
||||
-- definition D [private] (x y : A) (p : x = y) := p*(f x) = f y
|
||||
-- definition d [private] (x : A) : D x x (refl x)
|
||||
-- := refl (f x)
|
||||
|
||||
-- theorem apd {a b : A} (p : a = b) : p*(f a) = f b
|
||||
-- := path_rec (d a) p
|
||||
-- end
|
||||
|
||||
|
||||
-- abbreviation homotopy {A : Type} {P : A → Type} (f g : Π x, P x)
|
||||
-- := Π x, f x = g x
|
||||
|
||||
-- namespace logic
|
||||
-- infix `∼`:50 := homotopy
|
||||
-- end
|
||||
-- using logic
|
||||
|
||||
-- notation `assume` binders `,` r:(scoped f, f) := r
|
||||
-- notation `take` binders `,` r:(scoped f, f) := r
|
||||
|
||||
-- section
|
||||
-- parameters {A : Type} {B : Type}
|
||||
|
||||
-- theorem hom_refl (f : A → B) : f ∼ f
|
||||
-- := take x, refl (f x)
|
||||
|
||||
-- theorem hom_symm {f g : A → B} : f ∼ g → g ∼ f
|
||||
-- := assume h, take x, (h x)⁻¹
|
||||
|
||||
-- theorem hom_trans {f g h : A → B} : f ∼ g → g ∼ h → f ∼ h
|
||||
-- := assume h1 h2, take x, (h1 x) ⬝ (h2 x)
|
||||
|
||||
-- theorem hom_fun {f g : A → B} {x y : A} (H : f ∼ g) (p : x = y) : (H x) ⬝ (ap g p) = (ap f p) ⬝ (H y)
|
||||
-- := have e1 : (H x) ⬝ (refl (g x)) = (refl (f x)) ⬝ (H x), from
|
||||
-- calc (H x) ⬝ (refl (g x)) = H x : (trans_refl_right (H x))⁻¹
|
||||
-- ... = (refl (f x)) ⬝ (H x) : trans_refl_left (H x),
|
||||
-- have e2 : (H x) ⬝ (ap g (refl x)) = (ap f (refl x)) ⬝ (H x), from
|
||||
-- calc (H x) ⬝ (ap g (refl x)) = (H x) ⬝ (refl (g x)) : {ap_refl g x}
|
||||
-- ... = (refl (f x)) ⬝ (H x) : e1
|
||||
-- ... = (ap f (refl x)) ⬝ (H x) : {symm (ap_refl f x)},
|
||||
-- path_rec e2 p
|
||||
|
||||
|
||||
-- end
|
||||
|
||||
-- definition loop_space (A : Type) (a : A) := a = a
|
||||
-- notation `Ω` `(` A `,` a `)` := loop_space A a
|
||||
|
||||
-- definition loop2d_space (A : Type) (a : A) := (refl a) = (refl a)
|
||||
-- notation `Ω²` `(` A `,` a `)` := loop2d_space A a
|
||||
|
||||
-- inductive empty : Type
|
||||
|
||||
-- theorem empty_elim (c : Type) (H : empty) : c
|
||||
-- := empty_rec (λ e, c) H
|
||||
|
||||
-- definition not (A : Type) := A → empty
|
||||
-- prefix `¬`:40 := not
|
||||
|
||||
-- theorem not_intro {a : Type} (H : a → empty) : ¬ a
|
||||
-- := H
|
||||
|
||||
-- theorem not_elim {a : Type} (H1 : ¬ a) (H2 : a) : empty
|
||||
-- := H1 H2
|
||||
|
||||
-- theorem absurd {a : Type} (H1 : a) (H2 : ¬ a) : empty
|
||||
-- := H2 H1
|
||||
|
||||
-- theorem mt {a b : Type} (H1 : a → b) (H2 : ¬ b) : ¬ a
|
||||
-- := assume Ha : a, absurd (H1 Ha) H2
|
||||
|
||||
-- theorem contrapos {a b : Type} (H : a → b) : ¬ b → ¬ a
|
||||
-- := assume Hnb : ¬ b, mt H Hnb
|
||||
|
||||
-- theorem absurd_elim {a : Type} (b : Type) (H1 : a) (H2 : ¬ a) : b
|
||||
-- := empty_elim b (absurd H1 H2)
|
||||
|
||||
-- inductive unit : Type :=
|
||||
-- | star : unit
|
||||
|
||||
-- notation `⋆`:max := star
|
||||
|
||||
-- theorem absurd_not_unit (H : ¬ unit) : empty
|
||||
-- := absurd star H
|
||||
|
||||
-- theorem not_empty_trivial : ¬ empty
|
||||
-- := assume H : empty, H
|
||||
|
||||
-- theorem upun (x : unit) : x = ⋆
|
||||
-- := unit_rec (refl ⋆) x
|
||||
|
||||
-- inductive product (A : Type) (B : Type) : Type :=
|
||||
-- | pair : A → B → product A B
|
||||
|
||||
-- infixr `×`:30 := product
|
||||
-- infixr `∧`:30 := product
|
||||
|
||||
-- notation `(` h `,` t:(foldl `,` (e r, pair r e) h) `)` := t
|
||||
|
||||
-- definition pr1 {A : Type} {B : Type} (p : A × B) : A
|
||||
-- := product_rec (λ a b, a) p
|
||||
|
||||
-- definition pr2 {A : Type} {B : Type} (p : A × B) : B
|
||||
-- := product_rec (λ a b, b) p
|
||||
|
||||
-- theorem uppt {A : Type} {B : Type} (p : A × B) : (pr1 p, pr2 p) = p
|
||||
-- := product_rec (λ x y, refl (x, y)) p
|
||||
|
||||
-- inductive sum (A : Type) (B : Type) : Type :=
|
||||
-- | inl : A → sum A B
|
||||
-- | inr : B → sum A B
|
||||
|
||||
-- namespace logic
|
||||
-- infixr `+`:25 := sum
|
||||
-- end
|
||||
-- using logic
|
||||
-- infixr `∨`:25 := sum
|
||||
|
||||
-- theorem sum_elim {a : Type} {b : Type} {c : Type} (H1 : a + b) (H2 : a → c) (H3 : b → c) : c
|
||||
-- := sum_rec H2 H3 H1
|
||||
|
||||
-- theorem resolve_right {a : Type} {b : Type} (H1 : a + b) (H2 : ¬ a) : b
|
||||
-- := sum_elim H1 (assume Ha, absurd_elim b Ha H2) (assume Hb, Hb)
|
||||
|
||||
-- theorem resolve_left {a : Type} {b : Type} (H1 : a + b) (H2 : ¬ b) : a
|
||||
-- := sum_elim H1 (assume Ha, Ha) (assume Hb, absurd_elim a Hb H2)
|
||||
|
||||
-- theorem sum_flip {a : Type} {b : Type} (H : a + b) : b + a
|
||||
-- := sum_elim H (assume Ha, inr b Ha) (assume Hb, inl a Hb)
|
||||
|
||||
-- inductive Sigma {A : Type} (B : A → Type) : Type :=
|
||||
-- | sigma_intro : Π a, B a → Sigma B
|
||||
|
||||
-- notation `Σ` binders `,` r:(scoped P, Sigma P) := r
|
||||
|
||||
-- definition dpr1 {A : Type} {B : A → Type} (p : Σ x, B x) : A
|
||||
-- := Sigma_rec (λ a b, a) p
|
||||
|
||||
-- definition dpr2 {A : Type} {B : A → Type} (p : Σ x, B x) : B (dpr1 p)
|
||||
-- := Sigma_rec (λ a b, b) p
|
||||
|
|
@ -1,17 +0,0 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura
|
||||
import logic
|
||||
namespace num
|
||||
-- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26.
|
||||
-- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))).
|
||||
-- This representation can be coerced in whatever we want (e.g., naturals, integers, reals, etc).
|
||||
inductive pos_num : Type :=
|
||||
| one : pos_num
|
||||
| bit1 : pos_num → pos_num
|
||||
| bit0 : pos_num → pos_num
|
||||
|
||||
inductive num : Type :=
|
||||
| zero : num
|
||||
| pos : pos_num → num
|
||||
end num
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura
|
||||
import logic
|
||||
|
||||
definition is_prop (A : Type) := Π (x y : A), x = y
|
||||
|
||||
inductive hprop : Type :=
|
||||
| hprop_intro : Π (A : Type), is_prop A → hprop
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura
|
||||
import logic
|
||||
|
||||
definition is_set (A : Type) := Π (x y : A) (p q : x = y), p = q
|
||||
|
||||
inductive hset : Type :=
|
||||
| hset_intro : Π (A : Type), is_set A → hset
|
||||
|
|
@ -1,13 +0,0 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura
|
||||
import bool
|
||||
|
||||
namespace string
|
||||
inductive char : Type :=
|
||||
| ascii : bool → bool → bool → bool → bool → bool → bool → bool → char
|
||||
|
||||
inductive string : Type :=
|
||||
| empty : string
|
||||
| str : char → string → string
|
||||
end string
|
||||
|
|
@ -1,54 +0,0 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura
|
||||
import logic string num
|
||||
using string
|
||||
using num
|
||||
|
||||
namespace tactic
|
||||
-- This is just a trick to embed the 'tactic language' as a
|
||||
-- Lean expression. We should view 'tactic' as automation
|
||||
-- that when execute produces a term.
|
||||
-- builtin_tactic is just a "dummy" for creating the
|
||||
-- definitions that are actually implemented in C++
|
||||
inductive tactic : Type :=
|
||||
| builtin_tactic : tactic
|
||||
-- Remark the following names are not arbitrary, the tactic module
|
||||
-- uses them when converting Lean expressions into actual tactic objects.
|
||||
-- The bultin 'by' construct triggers the process of converting a
|
||||
-- a term of type 'tactic' into a tactic that sythesizes a term
|
||||
definition and_then (t1 t2 : tactic) : tactic := builtin_tactic
|
||||
definition or_else (t1 t2 : tactic) : tactic := builtin_tactic
|
||||
definition append (t1 t2 : tactic) : tactic := builtin_tactic
|
||||
definition interleave (t1 t2 : tactic) : tactic := builtin_tactic
|
||||
definition par (t1 t2 : tactic) : tactic := builtin_tactic
|
||||
definition fixpoint (f : tactic → tactic) : tactic := builtin_tactic
|
||||
definition repeat (t : tactic) : tactic := builtin_tactic
|
||||
definition at_most (t : tactic) (k : num) : tactic := builtin_tactic
|
||||
definition discard (t : tactic) (k : num) : tactic := builtin_tactic
|
||||
definition focus_at (t : tactic) (i : num) : tactic := builtin_tactic
|
||||
definition try_for (t : tactic) (ms : num) : tactic := builtin_tactic
|
||||
definition now : tactic := builtin_tactic
|
||||
definition assumption : tactic := builtin_tactic
|
||||
definition eassumption : tactic := builtin_tactic
|
||||
definition state : tactic := builtin_tactic
|
||||
definition fail : tactic := builtin_tactic
|
||||
definition id : tactic := builtin_tactic
|
||||
definition beta : tactic := builtin_tactic
|
||||
definition apply {B : Type} (b : B) : tactic := builtin_tactic
|
||||
definition unfold {B : Type} (b : B) : tactic := builtin_tactic
|
||||
definition exact {B : Type} (b : B) : tactic := builtin_tactic
|
||||
definition trace (s : string) : tactic := builtin_tactic
|
||||
precedence `;`:200
|
||||
infixl ; := and_then
|
||||
notation `!` t:max := repeat t
|
||||
-- [ t_1 | ... | t_n ] notation
|
||||
notation `[` h:100 `|` r:(foldl 100 `|` (e r, or_else r e) h) `]` := r
|
||||
-- [ t_1 || ... || t_n ] notation
|
||||
notation `[` h:100 `||` r:(foldl 100 `||` (e r, par r e) h) `]` := r
|
||||
definition try (t : tactic) : tactic := [ t | id ]
|
||||
notation `?` t:max := try t
|
||||
definition repeat1 (t : tactic) : tactic := t ; !t
|
||||
definition focus (t : tactic) : tactic := focus_at t 0
|
||||
definition determ (t : tactic) : tactic := at_most t 1
|
||||
end tactic
|
||||
|
|
@ -1,16 +1,11 @@
|
|||
----------------------------------------------------------------------------------------------------
|
||||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura
|
||||
----------------------------------------------------------------------------------------------------
|
||||
|
||||
import logic.connectives.basic logic.classes.decidable logic.classes.inhabited
|
||||
import .type logic.connectives.basic logic.classes.decidable logic.classes.inhabited
|
||||
using eq_proofs decidable
|
||||
|
||||
namespace bool
|
||||
inductive bool : Type :=
|
||||
| ff : bool
|
||||
| tt : bool
|
||||
|
||||
theorem induction_on {p : bool → Prop} (b : bool) (H0 : p ff) (H1 : p tt) : p b :=
|
||||
bool_rec H0 H1 b
|
||||
7
library/standard/data/bool/bool.md
Normal file
7
library/standard/data/bool/bool.md
Normal file
|
|
@ -0,0 +1,7 @@
|
|||
data.bool
|
||||
=========
|
||||
|
||||
The type of booleans.
|
||||
|
||||
* [type](type.lean) : the datatype
|
||||
* [basic](basic.lean) : basic properties
|
||||
5
library/standard/data/bool/default.lean
Normal file
5
library/standard/data/bool/default.lean
Normal file
|
|
@ -0,0 +1,5 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Jeremy Avigad
|
||||
|
||||
import .type .basic
|
||||
|
|
@ -1,6 +1,11 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura
|
||||
|
||||
namespace bool
|
||||
|
||||
inductive bool : Type :=
|
||||
| true : bool
|
||||
| false : bool
|
||||
| ff : bool
|
||||
| tt : bool
|
||||
|
||||
end bool
|
||||
|
|
@ -5,8 +5,9 @@ Various datatypes.
|
|||
|
||||
Basic types:
|
||||
|
||||
* [empty](empty.lean) : the empty type
|
||||
* [unit](unit.lean) : the singleton type
|
||||
* [bool](bool.lean)
|
||||
* [bool](bool/bool.md) : the boolean values
|
||||
* [num](num.lean) : generic numerals
|
||||
* [string](string.lean) : ascii strings
|
||||
* [nat](nat/nat.md) : the natural numbers
|
||||
|
|
|
|||
12
library/standard/data/empty.lean
Normal file
12
library/standard/data/empty.lean
Normal file
|
|
@ -0,0 +1,12 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Jeremy Avigad
|
||||
|
||||
-- TODO: add notation for negation (in the sense of homotopy type theory)
|
||||
|
||||
-- Empty type
|
||||
-- ----------
|
||||
|
||||
inductive empty : Type
|
||||
|
||||
theorem empty_elim (A : Type) (H : empty) : A := empty_rec (λe, A) H
|
||||
|
|
@ -1,7 +1,5 @@
|
|||
----------------------------------------------------------------------------------------------------
|
||||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Jeremy Avigad
|
||||
----------------------------------------------------------------------------------------------------
|
||||
|
||||
import data.list.basic
|
||||
|
|
|
|||
9
library/standard/general_notation.lean
Normal file
9
library/standard/general_notation.lean
Normal file
|
|
@ -0,0 +1,9 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura, Jeremy Avigad
|
||||
|
||||
-- General notation
|
||||
-- ----------------
|
||||
|
||||
notation `assume` binders `,` r:(scoped f, f) := r
|
||||
notation `take` binders `,` r:(scoped f, f) := r
|
||||
61
library/standard/hott/equiv.lean
Normal file
61
library/standard/hott/equiv.lean
Normal file
|
|
@ -0,0 +1,61 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Jeremy Avigad
|
||||
-- Ported from Coq HoTT
|
||||
|
||||
import .path
|
||||
|
||||
-- Equivalences
|
||||
-- ------------
|
||||
|
||||
abbreviation Sect {A B : Type} (s : A → B) (r : B → A) := Πx : A, r (s x) ≈ x
|
||||
|
||||
-- -- TODO: need better means of declaring structures
|
||||
-- -- TODO: note that Coq allows projections to be declared to be coercions on the fly
|
||||
|
||||
-- Structure IsEquiv
|
||||
|
||||
inductive IsEquiv {A B : Type} (f : A → B) :=
|
||||
| IsEquiv_mk : Π
|
||||
(equiv_inv : B → A)
|
||||
(eisretr : Sect equiv_inv f)
|
||||
(eissect : Sect f equiv_inv)
|
||||
(eisadj : Πx, eisretr (f x) ≈ ap f (eissect x)),
|
||||
IsEquiv f
|
||||
|
||||
definition equiv_inv {A B : Type} {f : A → B} (H : IsEquiv f) : B → A :=
|
||||
IsEquiv_rec (λequiv_inv eisretr eissect eisadj, equiv_inv) H
|
||||
|
||||
-- TODO: note: does not type check without giving the type
|
||||
definition eisretr {A B : Type} {f : A → B} (H : IsEquiv f) : Sect (equiv_inv H) f :=
|
||||
IsEquiv_rec (λequiv_inv eisretr eissect eisadj, eisretr) H
|
||||
|
||||
definition eissect {A B : Type} {f : A → B} (H : IsEquiv f) : Sect f (equiv_inv H) :=
|
||||
IsEquiv_rec (λequiv_inv eisretr eissect eisadj, eissect) H
|
||||
|
||||
definition eisadj {A B : Type} {f : A → B} (H : IsEquiv f) :
|
||||
Πx, eisretr H (f x) ≈ ap f (eissect H x) :=
|
||||
IsEquiv_rec (λequiv_inv eisretr eissect eisadj, eisadj) H
|
||||
|
||||
-- Structure Equiv
|
||||
|
||||
inductive Equiv (A B : Type) : Type :=
|
||||
| Equiv_mk : Π
|
||||
(equiv_fun : A → B)
|
||||
(equiv_isequiv : IsEquiv equiv_fun),
|
||||
Equiv A B
|
||||
|
||||
definition equiv_fun {A B : Type} (e : Equiv A B) : A → B :=
|
||||
Equiv_rec (λequiv_fun equiv_isequiv, equiv_fun) e
|
||||
|
||||
-- TODO: use a type class instead?
|
||||
coercion equiv_fun : Equiv
|
||||
|
||||
definition equiv_isequiv [coercion] {A B : Type} (e : Equiv A B) : IsEquiv (equiv_fun e) :=
|
||||
Equiv_rec (λequiv_fun equiv_isequiv, equiv_isequiv) e
|
||||
|
||||
-- coercion equiv_isequiv
|
||||
|
||||
-- TODO: better symbol
|
||||
infix `<~>`:25 := Equiv
|
||||
notation e `⁻¹`:75 := equiv_inv e
|
||||
21
library/standard/hott/funext.lean
Normal file
21
library/standard/hott/funext.lean
Normal file
|
|
@ -0,0 +1,21 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Jeremy Avigad
|
||||
-- Ported from Coq HoTT
|
||||
|
||||
-- TODO: move this to an "axioms" folder
|
||||
-- TODO: take a look at the Coq tricks
|
||||
|
||||
import .path .equiv
|
||||
|
||||
-- Funext
|
||||
-- ------
|
||||
|
||||
axiom funext {A : Type} {P : A → Type} (f g : Π x : A, P x) : IsEquiv (@apD10 A P f g)
|
||||
|
||||
definition path_forall {A : Type} {P : A → Type} (f g : Π x : A, P x) : f ∼ g → f ≈ g :=
|
||||
(funext f g)⁻¹
|
||||
|
||||
definition path_forall2 {A B : Type} {P : A → B → Type} (f g : Π x y, P x y) :
|
||||
(Πx y, f x y ≈ g x y) → f ≈ g :=
|
||||
λE, path_forall f g (λx, path_forall (f x) (g x) (E x))
|
||||
21
library/standard/hott/hott.md
Normal file
21
library/standard/hott/hott.md
Normal file
|
|
@ -0,0 +1,21 @@
|
|||
standard.hott
|
||||
=============
|
||||
|
||||
A library for Homotopy Type Theory, which avoid the use of prop. Many
|
||||
standard types are imported from `standard.data`, but then theorems
|
||||
are proved about them using predicate versions of the logical
|
||||
operations. For example, we use the path type, products, sums, sigmas,
|
||||
and the empty type, rather than equality, and, or, exists, and
|
||||
false. These operations take values in Type rather than Prop.
|
||||
|
||||
We view Homotopy Theory Theory as compatible with the axiomatic
|
||||
framework of Lean, simply ignoring the impredicative, proof irrelevant
|
||||
Prop. This is o.k. as long as we do not import additional axioms like
|
||||
propositional extensionality or Hilbert choice, which are incompatible
|
||||
with HoTT.
|
||||
|
||||
* [path](path.lean) : the path type and operations on paths
|
||||
* [equiv](equiv.lean) : equivalence of types
|
||||
* [trunc](trunc.lean) : truncatedness of types
|
||||
* [funext](funext.lean) : the functional extensionality axiom
|
||||
* [inhabited](inhabited.lean) : a predicative version of the inhabited class
|
||||
40
library/standard/hott/inhabited.lean
Normal file
40
library/standard/hott/inhabited.lean
Normal file
|
|
@ -0,0 +1,40 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura
|
||||
|
||||
-- The predicative version of inhabited
|
||||
-- TODO: restore instances
|
||||
|
||||
-- import logic bool
|
||||
-- using logic
|
||||
|
||||
namespace predicative
|
||||
|
||||
inductive inhabited (A : Type) : Type :=
|
||||
| inhabited_intro : A → inhabited A
|
||||
|
||||
theorem inhabited_elim {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B
|
||||
:= inhabited_rec H2 H1
|
||||
|
||||
end predicative
|
||||
|
||||
-- theorem inhabited_fun [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B)
|
||||
-- := inhabited_elim H (take (b : B), inhabited_intro (λ a : A, b))
|
||||
|
||||
-- theorem inhabited_sum_left [instance] {A : Type} (B : Type) (H : inhabited A) : inhabited (A + B)
|
||||
-- := inhabited_elim H (λ a, inhabited_intro (inl B a))
|
||||
|
||||
-- theorem inhabited_sum_right [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A + B)
|
||||
-- := inhabited_elim H (λ b, inhabited_intro (inr A b))
|
||||
|
||||
-- theorem inhabited_product [instance] {A : Type} {B : Type} (Ha : inhabited A) (Hb : inhabited B) : inhabited (A × B)
|
||||
-- := inhabited_elim Ha (λ a, (inhabited_elim Hb (λ b, inhabited_intro (a, b))))
|
||||
|
||||
-- theorem inhabited_bool [instance] : inhabited bool
|
||||
-- := inhabited_intro true
|
||||
|
||||
-- theorem inhabited_unit [instance] : inhabited unit
|
||||
-- := inhabited_intro ⋆
|
||||
|
||||
-- theorem inhabited_sigma_pr1 {A : Type} {B : A → Type} (p : Σ x, B x) : inhabited A
|
||||
-- := inhabited_intro (dpr1 p)
|
||||
|
|
@ -3,9 +3,9 @@
|
|||
-- Author: Jeremy Avigad
|
||||
-- Ported from Coq HoTT
|
||||
|
||||
import .logic .tactic
|
||||
import general_notation struc.function tools.tactic
|
||||
|
||||
using tactic
|
||||
using tactic function
|
||||
|
||||
-- Path
|
||||
-- ----
|
||||
38
library/standard/hott/trunc.lean
Normal file
38
library/standard/hott/trunc.lean
Normal file
|
|
@ -0,0 +1,38 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Jeremy Avigad
|
||||
-- Ported from Coq HoTT
|
||||
|
||||
import .path
|
||||
|
||||
|
||||
-- Truncation levels
|
||||
-- -----------------
|
||||
|
||||
inductive Contr (A : Type) : Type :=
|
||||
| Contr_mk : Π
|
||||
(center : A)
|
||||
(contr : Πy : A, center ≈ y),
|
||||
Contr A
|
||||
|
||||
definition center {A : Type} (C : Contr A) : A := Contr_rec (λcenter contr, center) C
|
||||
|
||||
definition contr {A : Type} (C : Contr A) : Πy : A, center C ≈ y :=
|
||||
Contr_rec (λcenter contr, contr) C
|
||||
|
||||
inductive trunc_index : Type :=
|
||||
| minus_two : trunc_index
|
||||
| trunc_S : trunc_index → trunc_index
|
||||
|
||||
-- TODO: add coercions to / from nat
|
||||
|
||||
-- TODO: note in the Coq version, there is an internal version
|
||||
definition IsTrunc (n : trunc_index) : Type → Type :=
|
||||
trunc_index_rec (λA, Contr A) (λn trunc_n A, (Π(x y : A), trunc_n (x ≈ y))) n
|
||||
|
||||
-- TODO: in the Coq version, this is notation
|
||||
abbreviation minus_one := trunc_S minus_two
|
||||
abbreviation IsHProp := IsTrunc minus_one
|
||||
abbreviation IsHSet := IsTrunc (trunc_S minus_one)
|
||||
|
||||
prefix `!`:75 := center
|
||||
|
|
@ -4,7 +4,7 @@
|
|||
-- Authors: Leonardo de Moura, Jeremy Avigad
|
||||
----------------------------------------------------------------------------------------------------
|
||||
|
||||
import .prop
|
||||
import general_notation .prop
|
||||
|
||||
-- implication
|
||||
-- -----------
|
||||
|
|
@ -26,9 +26,6 @@ inductive true : Prop :=
|
|||
abbreviation not (a : Prop) := a → false
|
||||
prefix `¬`:40 := not
|
||||
|
||||
notation `assume` binders `,` r:(scoped f, f) := r
|
||||
notation `take` binders `,` r:(scoped f, f) := r
|
||||
|
||||
|
||||
-- not
|
||||
-- ---
|
||||
|
|
|
|||
|
|
@ -9,4 +9,5 @@ Logical operations and connectives.
|
|||
* [cast](cast.lean) : casts and heterogeneous equality
|
||||
* [quantifiers](quantifiers.lean) : existential and universal quantifiers
|
||||
* [if](if.lean) : if-then-else
|
||||
* [instances](instances.lean) : type class instances
|
||||
* [instances](instances.lean) : type class instances
|
||||
* [examples](examples/examples.md)
|
||||
4
library/standard/logic/connectives/examples/examples.md
Normal file
4
library/standard/logic/connectives/examples/examples.md
Normal file
|
|
@ -0,0 +1,4 @@
|
|||
logic.connectives.examples
|
||||
==========================
|
||||
|
||||
* [instances_test](instances_test.lean)
|
||||
|
|
@ -0,0 +1,46 @@
|
|||
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
--- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
--- Author: Jeremy Avigad
|
||||
|
||||
import ..instances
|
||||
|
||||
using relation
|
||||
|
||||
|
||||
section
|
||||
|
||||
using relation.operations
|
||||
|
||||
theorem test1 (a b : Prop) (H : a ↔ b) (H1 : a) : b := mp H H1
|
||||
|
||||
end
|
||||
|
||||
|
||||
section
|
||||
|
||||
using gensubst
|
||||
|
||||
theorem test2 (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
|
||||
subst H1 H2
|
||||
|
||||
theorem test3 (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
|
||||
H1 ▸ H2
|
||||
|
||||
end
|
||||
|
||||
|
||||
theorem test4 (a b c d e : Prop) (H1 : a ↔ b) : (a ∨ c → ¬(d → a)) ↔ (b ∨ c → ¬(d → b)) :=
|
||||
congr.infer iff iff (λa, (a ∨ c → ¬(d → a))) H1
|
||||
|
||||
|
||||
section
|
||||
|
||||
using relation.symbols
|
||||
|
||||
theorem test5 (T : Type) (a b c d : T) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
|
||||
H1 ⬝ H2⁻¹ ⬝ H3
|
||||
|
||||
theorem test6 (a b c d : Prop) (H1 : a ↔ b) (H2 : c ↔ b) (H3 : c ↔ d) : a ↔ d :=
|
||||
H1 ⬝ (H2⁻¹ ⬝ H3)
|
||||
|
||||
end
|
||||
|
|
@ -1,8 +1,6 @@
|
|||
----------------------------------------------------------------------------------------------------
|
||||
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
--- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
--- Author: Jeremy Avigad
|
||||
----------------------------------------------------------------------------------------------------
|
||||
|
||||
import logic.connectives.basic logic.connectives.eq struc.relation
|
||||
|
||||
|
|
@ -71,7 +69,7 @@ theorem subst {T : Type} {R : T → T → Prop} {P : T → Prop} {C : congr.clas
|
|||
|
||||
infixr `▸`:75 := subst
|
||||
|
||||
end -- gensubst
|
||||
end gensubst
|
||||
|
||||
|
||||
-- = is an equivalence relation
|
||||
|
|
@ -107,51 +105,6 @@ theorem mp_like_iff [instance] (a b : Prop) (H : a ↔ b) : relation.mp_like.cla
|
|||
relation.mp_like.mk (iff_elim_left H)
|
||||
|
||||
|
||||
-- Tests
|
||||
-- -----
|
||||
|
||||
namespace logic_instances_tests
|
||||
|
||||
section
|
||||
|
||||
using relation.operations
|
||||
|
||||
theorem test1 (a b : Prop) (H : a ↔ b) (H1 : a) : b := mp H H1
|
||||
|
||||
end
|
||||
|
||||
|
||||
section
|
||||
|
||||
using gensubst
|
||||
|
||||
theorem test2 (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
|
||||
subst H1 H2
|
||||
|
||||
theorem test3 (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
|
||||
H1 ▸ H2
|
||||
|
||||
end
|
||||
|
||||
theorem test4 (a b c d e : Prop) (H1 : a ↔ b) : (a ∨ c → ¬(d → a)) ↔ (b ∨ c → ¬(d → b)) :=
|
||||
congr.infer iff iff (λa, (a ∨ c → ¬(d → a))) H1
|
||||
|
||||
|
||||
section
|
||||
|
||||
using relation.symbols
|
||||
|
||||
theorem test5 (T : Type) (a b c d : T) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
|
||||
H1 ⬝ H2⁻¹ ⬝ H3
|
||||
|
||||
theorem test6 (a b c d : Prop) (H1 : a ↔ b) (H2 : c ↔ b) (H3 : c ↔ d) : a ↔ d :=
|
||||
H1 ⬝ (H2⁻¹ ⬝ H3)
|
||||
|
||||
end
|
||||
|
||||
end
|
||||
|
||||
|
||||
-- Boolean calculations
|
||||
-- --------------------
|
||||
|
||||
|
|
|
|||
|
|
@ -1,7 +1,5 @@
|
|||
----------------------------------------------------------------------------------------------------
|
||||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura
|
||||
----------------------------------------------------------------------------------------------------
|
||||
|
||||
import logic tools.tactic data.num data.string data.pair logic.connectives.cast
|
||||
|
|
|
|||
|
|
@ -4,7 +4,9 @@ standard
|
|||
The Lean standard library. By default, `import standard` does not
|
||||
import the classical axioms. For that, use `import logic.axioms`.
|
||||
|
||||
* [general_notation](general_notation.lean) : notation shared by all libraries
|
||||
* [logic](logic/logic.md) : logical constructs and axioms
|
||||
* [data](data/data.md) : various datatypes
|
||||
* [struc](struc/struc.md) : axiomatic structures
|
||||
* [hott](hott/hott.md) : homotopy type theory
|
||||
* [tools](tools/tool.md) : various additional tools
|
||||
|
|
@ -26,7 +26,7 @@ abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : class R) : reflexive
|
|||
abbreviation infer ⦃T : Type⦄ {R : T → T → Type} {C : class R} : reflexive R
|
||||
:= class_rec (λu, u) C
|
||||
|
||||
end -- is_reflexive
|
||||
end is_reflexive
|
||||
|
||||
namespace is_symmetric
|
||||
|
||||
|
|
@ -39,7 +39,7 @@ abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : class R) ⦃x y : T
|
|||
abbreviation infer ⦃T : Type⦄ {R : T → T → Type} {C : class R} ⦃x y : T⦄ (H : R x y) : R y x
|
||||
:= class_rec (λu, u) C x y H
|
||||
|
||||
end -- is_symmetric
|
||||
end is_symmetric
|
||||
|
||||
namespace is_transitive
|
||||
|
||||
|
|
@ -54,7 +54,7 @@ abbreviation infer ⦃T : Type⦄ {R : T → T → Type} {C : class R} ⦃x y z
|
|||
(H2 : R y z) : R x z
|
||||
:= class_rec (λu, u) C x y z H1 H2
|
||||
|
||||
end -- is_transitive
|
||||
end is_transitive
|
||||
|
||||
|
||||
-- Congruence for unary and binary functions
|
||||
|
|
@ -113,9 +113,9 @@ theorem const {T2 : Type} (R2 : T2 → T2 → Prop) (H : relation.reflexive R2)
|
|||
class R1 R2 (λu : T1, c) :=
|
||||
mk (λx y H1, H c)
|
||||
|
||||
end -- namespace congr
|
||||
end congr
|
||||
|
||||
end -- namespace relation
|
||||
end relation
|
||||
|
||||
|
||||
-- TODO: notice these can't be in the congr namespace, if we want it visible without
|
||||
|
|
@ -147,7 +147,7 @@ definition app {R : Type → Type → Prop} {a : Type} {b : Type} {H : R a b}
|
|||
definition infer ⦃R : Type → Type → Prop⦄ {a : Type} {b : Type} (H : R a b)
|
||||
{C : class H} : a → b := class_rec (λx, x) C
|
||||
|
||||
end -- namespace mp_like
|
||||
end mp_like
|
||||
|
||||
|
||||
-- Notation for operations on general symbols
|
||||
|
|
@ -160,13 +160,13 @@ definition symm := is_symmetric.infer
|
|||
definition trans := is_transitive.infer
|
||||
definition mp := mp_like.infer
|
||||
|
||||
end -- namespace operations
|
||||
end operations
|
||||
|
||||
namespace symbols
|
||||
|
||||
postfix `⁻¹`:100 := operations.symm
|
||||
infixr `⬝`:75 := operations.trans
|
||||
|
||||
end -- namespace symbols
|
||||
end symbols
|
||||
|
||||
end -- namespace relation
|
||||
end relation
|
||||
|
|
|
|||
Loading…
Reference in a new issue