From c34c53ebb90824ceeb8e1aeeeaad41744d95e0a8 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 18 Feb 2021 12:32:15 +0000 Subject: [PATCH 1/9] feat(library/init/core): allow lists of proofs With upstream changes to mathlib, this would allow `fintype some_prop`, which would in turn allow proofs to be used to index finite things like matrices or summations. --- library/init/core.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/init/core.lean b/library/init/core.lean index 4c81a7e5fa..d0a0207a0b 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -334,14 +334,14 @@ def decidable_rel {α : Sort u} (r : α → α → Prop) := def decidable_eq (α : Sort u) := decidable_rel (@eq α) -inductive option (α : Type u) +inductive option (α : Sort u) | none : option | some (val : α) : option export option (none some) export bool (ff tt) -inductive list (T : Type u) +inductive list (T : Sort u) | nil : list | cons (hd : T) (tl : list) : list From fbf0f5f0e2fe55874220c23756fdd2fc2f025597 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 18 Feb 2021 13:19:43 +0000 Subject: [PATCH 2/9] Update has_reflect.lean --- library/init/meta/has_reflect.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/meta/has_reflect.lean b/library/init/meta/has_reflect.lean index 73850242df..a832346406 100644 --- a/library/init/meta/has_reflect.lean +++ b/library/init/meta/has_reflect.lean @@ -47,7 +47,7 @@ meta instance name.reflect : has_reflect name | (name.mk_string s n) := `(λ n, name.mk_string s n).subst (name.reflect n) | (name.mk_numeral i n) := `(λ n, name.mk_numeral i n).subst (name.reflect n) -meta instance list.reflect {α : Type} [has_reflect α] [reflected α] : has_reflect (list α) +meta instance list.reflect {α : Sort*} [has_reflect α] [reflected α] : has_reflect (list α) | [] := `([]) | (h::t) := `(λ t, h :: t).subst (list.reflect t) From 3d4a3bd0b35fccf16239ff99eb3ae12f7688e1be Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 18 Feb 2021 14:11:57 +0000 Subject: [PATCH 3/9] Update has_reflect.lean --- library/init/meta/has_reflect.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/library/init/meta/has_reflect.lean b/library/init/meta/has_reflect.lean index a832346406..e1f5f18819 100644 --- a/library/init/meta/has_reflect.lean +++ b/library/init/meta/has_reflect.lean @@ -47,7 +47,11 @@ meta instance name.reflect : has_reflect name | (name.mk_string s n) := `(λ n, name.mk_string s n).subst (name.reflect n) | (name.mk_numeral i n) := `(λ n, name.mk_numeral i n).subst (name.reflect n) -meta instance list.reflect {α : Sort*} [has_reflect α] [reflected α] : has_reflect (list α) +meta instance list.reflect' {α : Sort} [has_reflect α] [reflected α] : has_reflect (list α) +| [] := `([]) +| (h::t) := `(λ t, h :: t).subst (list.reflect' t) + +meta instance list.reflect {α : Type} [has_reflect α] [reflected α] : has_reflect (list α) | [] := `([]) | (h::t) := `(λ t, h :: t).subst (list.reflect t) From 058b3207ef4535220a1852a013b6e89cf0120a2c Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 18 Feb 2021 16:28:44 +0000 Subject: [PATCH 4/9] Update derive.lean --- library/init/meta/derive.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/meta/derive.lean b/library/init/meta/derive.lean index b91448e59e..3d1e879637 100644 --- a/library/init/meta/derive.lean +++ b/library/init/meta/derive.lean @@ -81,7 +81,7 @@ do decl ← get_decl n, else pure false @[derive_handler] meta def has_reflect_derive_handler := -instance_derive_handler ``has_reflect mk_has_reflect_instance ff (λ n params tgt, +instance_derive_handler ``has_reflect mk_has_reflect_instance tt (λ n params tgt, -- add additional `reflected` assumption for each parameter params.mfoldr (λ param tgt, do param_cls ← mk_app `reflected [param], From ef9f19903a4a9af0fc86ed68757ac24c6327d464 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 18 Feb 2021 16:50:20 +0000 Subject: [PATCH 5/9] Update has_reflect.lean --- library/init/meta/has_reflect.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/library/init/meta/has_reflect.lean b/library/init/meta/has_reflect.lean index e1f5f18819..a0e9f33f57 100644 --- a/library/init/meta/has_reflect.lean +++ b/library/init/meta/has_reflect.lean @@ -55,5 +55,10 @@ meta instance list.reflect {α : Type} [has_reflect α] [reflected α] : has_ref | [] := `([]) | (h::t) := `(λ t, h :: t).subst (list.reflect t) +-- `has_reflect_derive_handler` only generates this for `Sort` +meta instance option.reflect {α : Type} [has_reflect α] [reflected α] : has_reflect (option α) +| none := `(none) +| (some x) := `(some x) + meta instance punit.reflect : has_reflect punit | () := `(_) From 0c8fc6493cd1f918e6b81cf5a20146870760f8b4 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 18 Feb 2021 16:50:42 +0000 Subject: [PATCH 6/9] Update library/init/meta/derive.lean --- library/init/meta/derive.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/meta/derive.lean b/library/init/meta/derive.lean index 3d1e879637..b91448e59e 100644 --- a/library/init/meta/derive.lean +++ b/library/init/meta/derive.lean @@ -81,7 +81,7 @@ do decl ← get_decl n, else pure false @[derive_handler] meta def has_reflect_derive_handler := -instance_derive_handler ``has_reflect mk_has_reflect_instance tt (λ n params tgt, +instance_derive_handler ``has_reflect mk_has_reflect_instance ff (λ n params tgt, -- add additional `reflected` assumption for each parameter params.mfoldr (λ param tgt, do param_cls ← mk_app `reflected [param], From 47841a5fc0a74a7e8b17ba1a9ed04ecedacc019b Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 18 Feb 2021 17:07:24 +0000 Subject: [PATCH 7/9] Update interactive.lean --- library/init/meta/interactive.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 9b8049d131..1464f1d0b9 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -1206,7 +1206,8 @@ do (hs, gex, hex, all_hyps) ← decode_simp_arg_list_with_symm hs, when (all_hyps ∧ at_star ∧ not hex.empty) $ fail "A tactic of the form `simp [*, -h] at *` is currently not supported", s ← join_user_simp_lemmas no_dflt attr_names, -- Erase `h` from the default simp set for calls of the form `simp [←h]`. - let to_erase := hs.foldl (λ l h, match h with + let to_erase : list pname := + hs.foldl (λ l h, match h with | (const id _, tt) := id :: l | (local_const id _ _ _, tt) := id :: l | _ := l From dc73832b9549eaa9cb8be431d2ed0a8d84ea8806 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 18 Feb 2021 17:08:12 +0000 Subject: [PATCH 8/9] Update library/init/meta/interactive.lean --- library/init/meta/interactive.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 1464f1d0b9..38f3f84dd0 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -1206,7 +1206,7 @@ do (hs, gex, hex, all_hyps) ← decode_simp_arg_list_with_symm hs, when (all_hyps ∧ at_star ∧ not hex.empty) $ fail "A tactic of the form `simp [*, -h] at *` is currently not supported", s ← join_user_simp_lemmas no_dflt attr_names, -- Erase `h` from the default simp set for calls of the form `simp [←h]`. - let to_erase : list pname := + let to_erase : list name := hs.foldl (λ l h, match h with | (const id _, tt) := id :: l | (local_const id _ _ _, tt) := id :: l From 32029282d498f887afcb9f60c9d608c1c6f18c84 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 18 Feb 2021 17:29:27 +0000 Subject: [PATCH 9/9] Update lemmas.lean --- library/init/data/list/lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/data/list/lemmas.lean b/library/init/data/list/lemmas.lean index 226beffa0b..3f9a746847 100644 --- a/library/init/data/list/lemmas.lean +++ b/library/init/data/list/lemmas.lean @@ -8,7 +8,7 @@ import init.data.list.basic init.function init.meta init.data.nat.lemmas import init.meta.interactive init.meta.smt.rsimp universes u v w w₁ w₂ -variables {α : Type u} {β : Type v} {γ : Type w} +variables {α : Sort u} {β : Sort v} {γ : Sort w} namespace list open nat