From d9ee994281cb082f1be2e27744f1f72a0e502114 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 26 Jul 2014 19:13:04 -0700 Subject: [PATCH] feat(library/hott): copy basic files to hott library Signed-off-by: Leonardo de Moura --- library/hott/bool.lean | 6 +++++ library/hott/inhabited.lean | 2 +- library/hott/logic.lean | 7 ----- library/hott/num.lean | 17 ++++++++++++ library/hott/string.lean | 13 +++++++++ library/hott/tactic.lean | 54 +++++++++++++++++++++++++++++++++++++ 6 files changed, 91 insertions(+), 8 deletions(-) create mode 100644 library/hott/bool.lean create mode 100644 library/hott/num.lean create mode 100644 library/hott/string.lean create mode 100644 library/hott/tactic.lean diff --git a/library/hott/bool.lean b/library/hott/bool.lean new file mode 100644 index 000000000..61d2c680d --- /dev/null +++ b/library/hott/bool.lean @@ -0,0 +1,6 @@ +-- Copyright (c) 2014 Microsoft Corporation. All rights reserved. +-- Released under Apache 2.0 license as described in the file LICENSE. +-- Author: Leonardo de Moura +inductive bool : Type := +| true : bool +| false : bool diff --git a/library/hott/inhabited.lean b/library/hott/inhabited.lean index 1353de977..cb609329b 100644 --- a/library/hott/inhabited.lean +++ b/library/hott/inhabited.lean @@ -1,7 +1,7 @@ -- 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 +import logic bool using logic inductive inhabited (A : Type) : Type := diff --git a/library/hott/logic.lean b/library/hott/logic.lean index 5b263f374..5c47a79f4 100644 --- a/library/hott/logic.lean +++ b/library/hott/logic.lean @@ -231,13 +231,6 @@ theorem resolve_left {a : Type} {b : Type} (H1 : a + b) (H2 : ¬ b) : a 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 bool : Type := -| true : bool -| false : bool - -theorem bool_cases (p : bool) : p = true ∨ p = false -:= bool_rec (inl _ (refl true)) (inr _ (refl false)) p - inductive Sigma {A : Type} (B : A → Type) : Type := | sigma_intro : Π a, B a → Sigma B diff --git a/library/hott/num.lean b/library/hott/num.lean new file mode 100644 index 000000000..f2f5577a9 --- /dev/null +++ b/library/hott/num.lean @@ -0,0 +1,17 @@ +-- 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 \ No newline at end of file diff --git a/library/hott/string.lean b/library/hott/string.lean new file mode 100644 index 000000000..9c168d2c6 --- /dev/null +++ b/library/hott/string.lean @@ -0,0 +1,13 @@ +-- 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 diff --git a/library/hott/tactic.lean b/library/hott/tactic.lean new file mode 100644 index 000000000..676ca800e --- /dev/null +++ b/library/hott/tactic.lean @@ -0,0 +1,54 @@ +-- 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