max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(library): add has_append type class, string concatenation is now an instance of has_append instead of has_add

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-27 07:58:17 +01:00
parent f3803c6ee4
commit 9aa6ac62ec
20 changed files with 81 additions and 75 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/data/list/perm.lean
View file

@ -97,7 +97,7 @@ list.induction_on l
(λ p, p)
(λ x xs r p, skip x (r p))
theorem perm_app [congr] {l₁ l₂ t₁ t₂ : list A} : l₁ ~ l₂ → t₁ ~ t₂ → (l₁++t₁) ~ (l₂++t₂) :=
theorem perm_app {l₁ l₂ t₁ t₂ : list A} : l₁ ~ l₂ → t₁ ~ t₂ → (l₁++t₁) ~ (l₂++t₂) :=
assume p₁ p₂, trans (perm_app_left t₁ p₁) (perm_app_right l₂ p₂)
theorem perm_app_cons (a : A) {h₁ h₂ t₁ t₂ : list A} : h₁ ~ h₂ → t₁ ~ t₂ → (h₁ ++ (a::t₁)) ~ (h₂ ++ (a::t₂)) :=

5
library/init/list.lean
View file

@ -36,8 +36,6 @@ definition append : list A → list A → list A
| [] l := l
| (h :: s) t := h :: (append s t)
notation l₁ ++ l₂ := append l₁ l₂
definition length : list A → nat
| [] := 0
| (a :: l) := length l + 1
@ -54,3 +52,6 @@ definition tail : list A → list A
| (a :: l) := l
end list
definition list_has_append [instance] {A : Type} : has_append (list A) :=
has_append.mk list.append

2
library/init/meta/base_tactic.lean
View file

@ -22,7 +22,7 @@ variables [has_to_string A]
protected meta_definition base_tactic_result.to_string : base_tactic_result S A → string
| (success a s) := to_string a
| (exception A e s) := "Exception: " + to_string (e options.mk)
| (exception A e s) := "Exception: " ++ to_string (e options.mk)
protected meta_definition base_tactic_result.has_to_string [instance] : has_to_string (base_tactic_result S A) :=
has_to_string.mk base_tactic_result.to_string

2
library/init/meta/exceptional.lean
View file

@ -20,7 +20,7 @@ variables [has_to_string A]
protected meta_definition exceptional.to_string : exceptional A → string
| (success a) := to_string a
| (exception A e) := "Exception: " + to_string (e options.mk)
| (exception A e) := "Exception: " ++ to_string (e options.mk)
protected meta_definition exceptional.has_to_string [instance] : has_to_string (exceptional A) :=
has_to_string.mk exceptional.to_string

4
library/init/meta/name.lean
View file

@ -37,8 +37,8 @@ definition name.to_string : name → string
| anonymous := "[anonymous]"
| (mk_string s anonymous) := s
| (mk_numeral v anonymous) := to_string v
| (mk_string s n) := name.to_string n + "." + s
| (mk_numeral v n) := name.to_string n + "." + to_string v
| (mk_string s n) := name.to_string n ++ "." ++ s
| (mk_numeral v n) := name.to_string n ++ "." ++ to_string v
definition name.has_to_string [instance] : has_to_string name :=
has_to_string.mk name.to_string

4
library/init/meta/rb_map.lean
View file

@ -60,9 +60,9 @@ end
section
variables {key : Type} {data : Type} [has_to_string key] [has_to_string data]
private meta_definition key_data_to_string (k : key) (d : data) (first : bool) : string :=
(if first = tt then "" else ", ") + to_string k + " ← " + to_string d
(if first = tt then "" else ", ") ++ to_string k ++ " ← " ++ to_string d
meta_definition rb_map_has_to_string [instance] : has_to_string (rb_map key data) :=
has_to_string.mk (λ m,
"⟨" + (pr₁ (fold m ("", tt) (λ k d p, (pr₁ p + key_data_to_string k d (pr₂ p), ff)))) + "⟩")
"⟨" ++ (pr₁ (fold m ("", tt) (λ k d p, (pr₁ p ++ key_data_to_string k d (pr₂ p), ff)))) ++ "⟩")
end

2
library/init/meta/relation_tactics.lean
View file

@ -15,7 +15,7 @@ do tgt ← target,
r ← return $ get_app_fn tgt,
match op_for env (const_name r) with
| some refl := mk_const refl >>= apply
| none := fail (tac_name + " tactic failed, target is not a reflexive relation application")
| none := fail (tac_name ++ " tactic failed, target is not a reflexive relation application")
end
meta_definition reflexivity : tactic unit :=

51
library/init/reserved_notation.lean
View file

@ -9,31 +9,33 @@ import init.datatypes
notation `assume` binders `,` r:(scoped f, f) := r
notation `take` binders `,` r:(scoped f, f) := r
structure has_zero [class] (A : Type) := (zero : A)
structure has_one [class] (A : Type) := (one : A)
structure has_add [class] (A : Type) := (add : A → A → A)
structure has_mul [class] (A : Type) := (mul : A → A → A)
structure has_inv [class] (A : Type) := (inv : A → A)
structure has_neg [class] (A : Type) := (neg : A → A)
structure has_sub [class] (A : Type) := (sub : A → A → A)
structure has_div [class] (A : Type) := (div : A → A → A)
structure has_dvd [class] (A : Type) := (dvd : A → A → Prop)
structure has_mod [class] (A : Type) := (mod : A → A → A)
structure has_le [class] (A : Type) := (le : A → A → Prop)
structure has_lt [class] (A : Type) := (lt : A → A → Prop)
structure has_zero [class] (A : Type) := (zero : A)
structure has_one [class] (A : Type) := (one : A)
structure has_add [class] (A : Type) := (add : A → A → A)
structure has_mul [class] (A : Type) := (mul : A → A → A)
structure has_inv [class] (A : Type) := (inv : A → A)
structure has_neg [class] (A : Type) := (neg : A → A)
structure has_sub [class] (A : Type) := (sub : A → A → A)
structure has_div [class] (A : Type) := (div : A → A → A)
structure has_dvd [class] (A : Type) := (dvd : A → A → Prop)
structure has_mod [class] (A : Type) := (mod : A → A → A)
structure has_le [class] (A : Type) := (le : A → A → Prop)
structure has_lt [class] (A : Type) := (lt : A → A → Prop)
structure has_append [class] (A : Type) := (append : A → A → A)
definition zero {A : Type} [s : has_zero A] : A := has_zero.zero A
definition one {A : Type} [s : has_one A] : A := has_one.one A
definition add {A : Type} [s : has_add A] : A → A → A := has_add.add
definition mul {A : Type} [s : has_mul A] : A → A → A := has_mul.mul
definition sub {A : Type} [s : has_sub A] : A → A → A := has_sub.sub
definition div {A : Type} [s : has_div A] : A → A → A := has_div.div
definition dvd {A : Type} [s : has_dvd A] : A → A → Prop := has_dvd.dvd
definition mod {A : Type} [s : has_mod A] : A → A → A := has_mod.mod
definition neg {A : Type} [s : has_neg A] : A → A := has_neg.neg
definition inv {A : Type} [s : has_inv A] : A → A := has_inv.inv
definition le {A : Type} [s : has_le A] : A → A → Prop := has_le.le
definition lt {A : Type} [s : has_lt A] : A → A → Prop := has_lt.lt
definition zero {A : Type} [has_zero A] : A := has_zero.zero A
definition one {A : Type} [has_one A] : A := has_one.one A
definition add {A : Type} [has_add A] : A → A → A := has_add.add
definition mul {A : Type} [has_mul A] : A → A → A := has_mul.mul
definition sub {A : Type} [has_sub A] : A → A → A := has_sub.sub
definition div {A : Type} [has_div A] : A → A → A := has_div.div
definition dvd {A : Type} [has_dvd A] : A → A → Prop := has_dvd.dvd
definition mod {A : Type} [has_mod A] : A → A → A := has_mod.mod
definition neg {A : Type} [has_neg A] : A → A := has_neg.neg
definition inv {A : Type} [has_inv A] : A → A := has_inv.inv
definition le {A : Type} [has_le A] : A → A → Prop := has_le.le
definition lt {A : Type} [has_lt A] : A → A → Prop := has_lt.lt
definition append {A : Type} [has_append A] : A → A → A := has_append.append
definition ge [reducible] {A : Type} [s : has_le A] (a b : A) : Prop := le b a
definition gt [reducible] {A : Type} [s : has_lt A] (a b : A) : Prop := lt b a
@ -211,6 +213,7 @@ infix ≤ := le
infix ≥ := ge
infix < := lt
infix > := gt
infix ++ := append
notation [parsing_only] x ` +[`:65 A:0 `] `:0 y:65 := @add A _ x y
notation [parsing_only] x ` -[`:65 A:0 `] `:0 y:65 := @sub A _ x y

4
library/init/string.lean
View file

@ -16,5 +16,5 @@ definition concat (a b : string) : string :=
list.append b a
end string
definition string.has_add [instance] : has_add string :=
has_add.mk string.concat
definition string.has_append [instance] : has_append string :=
has_append.mk string.concat

22
library/init/to_string.lean
View file

@ -19,12 +19,12 @@ has_to_string.mk (λ b, if p then "tt" else "ff")
definition list.to_string_aux {A : Type} [has_to_string A] : bool → list A → string
| _ [] := ""
| tt (x::xs) := to_string x + list.to_string_aux ff xs
| ff (x::xs) := ", " + to_string x + list.to_string_aux ff xs
| tt (x::xs) := to_string x ++ list.to_string_aux ff xs
| ff (x::xs) := ", " ++ to_string x ++ list.to_string_aux ff xs
definition list.to_string {A : Type} [has_to_string A] : list A → string
| [] := "[]"
| (x::xs) := "[" + list.to_string_aux tt (x::xs) + "]"
| (x::xs) := "[" ++ list.to_string_aux tt (x::xs) ++ "]"
definition list.has_to_string [instance] {A : Type} [has_to_string A] : has_to_string (list A) :=
has_to_string.mk list.to_string
@ -33,17 +33,17 @@ definition unit.has_to_string [instance] : has_to_string unit :=
has_to_string.mk (λ u, "star")
definition option.has_to_string [instance] {A : Type} [has_to_string A] : has_to_string (option A) :=
has_to_string.mk (λ o, match o with | none := "none" | some a := "(some " + to_string a + ")" end)
has_to_string.mk (λ o, match o with | none := "none" | some a := "(some " ++ to_string a ++ ")" end)
definition sum.has_to_string [instance] {A B : Type} [has_to_string A] [has_to_string B] : has_to_string (sum A B) :=
has_to_string.mk (λ s, match s with | inl a := "(inl " + to_string a + ")" | inr b := "(inr " + to_string b + ")" end)
has_to_string.mk (λ s, match s with | inl a := "(inl " ++ to_string a ++ ")" | inr b := "(inr " ++ to_string b ++ ")" end)
definition prod.has_to_string [instance] {A B : Type} [has_to_string A] [has_to_string B] : has_to_string (prod A B) :=
has_to_string.mk (λ p, "(" + to_string (pr1 p) + ", " + to_string (pr2 p) + ")")
has_to_string.mk (λ p, "(" ++ to_string (pr1 p) ++ ", " ++ to_string (pr2 p) ++ ")")
definition sigma.has_to_string [instance] {A : Type} {B : A → Type} [has_to_string A] [s : ∀ x, has_to_string (B x)]
: has_to_string (sigma B) :=
has_to_string.mk (λ p, "⟨" + to_string (pr1 p) + ", " + to_string (pr2 p) + "⟩")
has_to_string.mk (λ p, "⟨" ++ to_string (pr1 p) ++ ", " ++ to_string (pr2 p) ++ "⟩")
definition subtype.has_to_string [instance] {A : Type} {P : A → Prop} [has_to_string A] : has_to_string (subtype P) :=
has_to_string.mk (λ s, to_string (elt_of s))
@ -55,15 +55,15 @@ else if char.to_nat c = 34 then "\\\""
else c::nil
definition char.has_to_sting [instance] : has_to_string char :=
has_to_string.mk (λ c, "'" + char.quote_core c + "'")
has_to_string.mk (λ c, "'" ++ char.quote_core c ++ "'")
definition string.quote_aux : string → string
| [] := ""
| (x::xs) := string.quote_aux xs + char.quote_core x
| (x::xs) := string.quote_aux xs ++ char.quote_core x
definition string.quote : string → string
| [] := "\"\""
| (x::xs) := "\"" + string.quote_aux (x::xs) + "\""
| (x::xs) := "\"" ++ string.quote_aux (x::xs) ++ "\""
definition string.has_to_string [instance] : has_to_string string :=
has_to_string.mk string.quote
@ -71,7 +71,7 @@ has_to_string.mk string.quote
/- Remark: the code generator replaces this definition with one that display natural numbers in decimal notation -/
definition nat.to_string : nat → string
| 0 := "zero"
| (succ a) := "(succ " + nat.to_string a + ")"
| (succ a) := "(succ " ++ nat.to_string a ++ ")"
definition nat.has_to_string [instance] : has_to_string nat :=
has_to_string.mk nat.to_string

2
tests/lean/local_notation_bug.lean.expected.out
View file

@ -8,7 +8,7 @@ expr ↣ _Fun : expr.app
string ↣ name : mk_simple_name
expr ↣ [fun-class] : expr.app
10 : ?M_1
local_notation_bug.lean:22:8: error: invalid expression
local_notation_bug.lean:22:10: error: invalid expression
expr ↣ _Fun : expr.app
string ↣ name : mk_simple_name
expr ↣ [fun-class] : expr.app

2
tests/lean/run/arity1.lean
View file

@ -13,6 +13,6 @@ by do
bla ← mk_const "bla",
infer_type bla >>= trace,
n ← get_arity bla,
trace ("n arity: " + to_string n),
trace ("n arity: " ++ to_string n),
when (n ≠ 3) (fail "bla is expected to have arity 3"),
constructor

12
tests/lean/run/eq15.lean
View file

@ -3,15 +3,15 @@ open list
set_option pp.implicit true
definition append : Π {A : Type}, list A → list A → list A
| append nil l := l
| append (h :: t) l := h :: (append t l)
definition app : Π {A : Type}, list A → list A → list A
| app nil l := l
| app (h :: t) l := h :: (app t l)
theorem append_nil {A : Type} (l : list A) : append nil l = l :=
theorem app_nil {A : Type} (l : list A) : app nil l = l :=
rfl
theorem append_cons {A : Type} (h : A) (t l : list A) : append (h :: t) l = h :: (append t l) :=
theorem app_cons {A : Type} (h : A) (t l : list A) : app (h :: t) l = h :: (app t l) :=
rfl
example : append ((1:nat) :: 2 :: nil) (3 :: 4 :: 5 :: nil) = (1 :: 2 :: 3 :: 4 :: 5 :: nil) :=
example : app ((1:nat) :: 2 :: nil) (3 :: 4 :: 5 :: nil) = (1 :: 2 :: 3 :: 4 :: 5 :: nil) :=
rfl

12
tests/lean/run/eq16.lean
View file

@ -4,15 +4,15 @@ open list
variable {A : Type}
set_option pp.implicit true
definition append : list A → list A → list A
| append nil l := l
| append (h :: t) l := h :: (append t l)
definition app : list A → list A → list A
| app nil l := l
| app (h :: t) l := h :: (app t l)
theorem append_nil (l : list A) : append nil l = l :=
theorem app_nil (l : list A) : app nil l = l :=
rfl
theorem append_cons (h : A) (t l : list A) : append (h :: t) l = h :: (append t l) :=
theorem app_cons (h : A) (t l : list A) : app (h :: t) l = h :: (app t l) :=
rfl
example : append ((1:num) :: 2 :: nil) (3 :: 4 :: 5 :: nil) = (1 :: 2 :: 3 :: 4 :: 5 :: nil) :=
example : app ((1:num) :: 2 :: nil) (3 :: 4 :: 5 :: nil) = (1 :: 2 :: 3 :: 4 :: 5 :: nil) :=
rfl

12
tests/lean/run/eq6.lean
View file

@ -1,15 +1,15 @@
import data.list
open list
definition append {A : Type} : list A → list A → list A
| append nil l := l
| append (h :: t) l := h :: (append t l)
definition appd {A : Type} : list A → list A → list A
| appd nil l := l
| appd (h :: t) l := h :: (appd t l)
theorem append_nil {A : Type} (l : list A) : append nil l = l :=
theorem appd_nil {A : Type} (l : list A) : appd nil l = l :=
rfl
theorem append_cons {A : Type} (h : A) (t l : list A) : append (h :: t) l = h :: (append t l) :=
theorem appd_cons {A : Type} (h : A) (t l : list A) : appd (h :: t) l = h :: (appd t l) :=
rfl
example : append ((1:nat) :: 2 :: nil) (3 :: 4 :: 5 :: nil) = (1 :: 2 :: 3 :: 4 :: 5 :: nil) :=
example : appd ((1:nat) :: 2 :: nil) (3 :: 4 :: 5 :: nil) = (1 :: 2 :: 3 :: 4 :: 5 :: nil) :=
rfl

4
tests/lean/run/meta_tac6.lean
View file

@ -16,12 +16,12 @@ by do
fmt₂ ← pp t,
trace $ fmt₁ + to_fmt " : " + fmt₂),
trace "----------",
trace $ "num: " + to_string n,
trace $ "num: " ++ to_string n,
trace_state,
get_local "H3" >>= clear,
(do {get_local "H3", return ()} <|> trace "get_local failed"),
trace_state,
assumption,
n : nat ← num_goals,
trace $ "num: " + to_string n,
trace $ "num: " ++ to_string n,
return ()

6
tests/lean/sec_notation2.lean
View file

@ -11,16 +11,16 @@ section
postfix `+.2`:100 := add2
local postfix `++2`:100 := add2
local postfix `**2`:100 := add2
eval 3 +.2
example : 3 +.2 = 3 ++2 := rfl
example : 3 +.2 = 3 **2 := rfl
end
eval 3 +.2
example : 3 +.2 = 3 ++2 := rfl -- error
example : 3 +.2 = 3 **2 := rfl -- error
end

2
tests/lean/sec_notation2.lean.expected.out
View file

@ -1,5 +1,5 @@
5
5
sec_notation2.lean:23:21: error: invalid expression
sec_notation2.lean:23:22: error: invalid expression
5
sec_notation2.lean:30:13: error: invalid expression

4
tests/lean/str1.lean.expected.out
View file

@ -4,11 +4,11 @@
"AB" : list char
"ABC" : list char
"abcD" : list char
"abc" ++ "cde" : list char
append "abc" "cde" : list char
str 67 (str 66 (str 65 empty)) : string
str 68 (str 65 (str 66 (str 99 (str 98 (str 97 empty))))) : string
65 :: str 99 (str 98 (str 97 empty)) : list char
[66, 65] : list char
[67, 66, 65] : list char
68 :: str 99 (str 98 (str 97 empty)) : list char
str 99 (str 98 (str 97 empty)) ++ str 101 (str 100 (str 99 empty)) : list char
append (str 99 (str 98 (str 97 empty))) (str 101 (str 100 (str 99 empty))) : list char

2
tests/lean/struct_class.lean.expected.out
View file

@ -1,6 +1,7 @@
decidable : Prop → Type₁
functor : (Type → Type) → Type
has_add : Type → Type
has_append : Type → Type
has_div : Type → Type
has_dvd : Type → Type
has_inv : Type → Type
@ -28,6 +29,7 @@ well_founded : Π {A}, (A → A → Prop) → Prop
decidable : Prop → Type₁
functor : (Type → Type) → Type
has_add : Type → Type
has_append : Type → Type
has_div : Type → Type
has_dvd : Type → Type
has_inv : Type → Type