michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/structure_cmd): remove 'cases_on' for structures since it may confuse users, add 'destruct' as alternative name for 'rec_on'

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-03 23:06:33 -08:00
parent 7897e21a14
commit b24165dc7b
5 changed files with 14 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/data/prod.lean
View file

@ -20,8 +20,6 @@ namespace prod
notation `(` h `,` t:(foldl `,` (e r, prod.mk r e) h) `)` := t
variables {A B : Type}
protected theorem destruct {P : A × B → Prop} (p : A × B) (H : ∀a b, P (a, b)) : P p :=
rec H p
notation `pr₁` := pr1
notation `pr₂` := pr2

3
library/data/sigma.lean
View file

@ -16,9 +16,6 @@ namespace sigma
theorem dpr1_dpair (a : A) (b : B a) : dpr1 (dpair a b) = a := rfl
theorem dpr2_dpair (a : A) (b : B a) : dpr2 (dpair a b) = b := rfl
protected theorem destruct {P : sigma B → Prop} (p : sigma B) (H : ∀a b, P (dpair a b)) : P p :=
rec H p
theorem dpair_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) :
dpair a₁ b₁ = dpair a₂ b₂ :=
dcongr_arg2 dpair H₁ H₂

18
src/frontends/lean/structure_cmd.cpp
View file

@ -28,7 +28,6 @@ Author: Leonardo de Moura
#include "library/definitional/rec_on.h"
#include "library/definitional/induction_on.h"
#include "library/definitional/cases_on.h"
#include "library/definitional/unit.h"
#include "library/definitional/eq.h"
#include "library/definitional/projection.h"
#include "frontends/lean/parser.h"
@ -597,7 +596,6 @@ struct structure_cmd_fn {
}
void declare_auxiliary() {
bool has_unit = has_unit_decls(m_env);
m_env = mk_rec_on(m_env, m_name);
m_env = mk_induction_on(m_env, m_name);
name rec_on_name(m_name, "rec_on");
@ -606,12 +604,16 @@ struct structure_cmd_fn {
add_rec_alias(induction_on_name);
save_def_info(rec_on_name);
save_def_info(induction_on_name);
if (has_unit) {
m_env = mk_cases_on(m_env, m_name);
name cases_on_name(m_name, "cases_on");
save_def_info(cases_on_name);
add_rec_alias(cases_on_name);
}
name destruct_name(m_name, "destruct");
bool opaque = false;
declaration rec_on_decl = m_env.get(rec_on_name);
declaration destruct_decl = mk_definition(m_env, destruct_name, rec_on_decl.get_univ_params(),
rec_on_decl.get_type(), rec_on_decl.get_value(),
opaque);
m_env = module::add(m_env, check(m_env, destruct_decl));
m_env = set_reducible(m_env, destruct_name, reducible_status::On);
save_def_info(destruct_name);
add_alias(destruct_name);
}
void declare_coercions() {

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

@ -11,7 +11,7 @@ check point.x
check point.y
check point.rec_on
check point.induction_on
check point.cases_on
check point.destruct
inductive color :=
red, green, blue

6
tests/lean/run/sigma_no_confusion.lean
View file

@ -2,15 +2,15 @@ import data.sigma tools.tactic
namespace sigma
definition no_confusion_type {A : Type} {B : A → Type} (P : Type) (v₁ v₂ : sigma B) : Type :=
cases_on v₁
(λ (a₁ : A) (b₁ : B a₁), cases_on v₂
rec_on v₁
(λ (a₁ : A) (b₁ : B a₁), rec_on v₂
(λ (a₂ : A) (b₂ : B a₂),
(Π (eq₁ : a₁ = a₂), eq.rec_on eq₁ b₁ = b₂ → P) → P))
definition no_confusion {A : Type} {B : A → Type} {P : Type} {v₁ v₂ : sigma B} : v₁ = v₂ → no_confusion_type P v₁ v₂ :=
assume H₁₂ : v₁ = v₂,
have aux : v₁ = v₁ → no_confusion_type P v₁ v₁, from
assume H₁₁, cases_on v₁
assume H₁₁, rec_on v₁
(λ (a₁ : A) (b₁ : B a₁) (h : Π (eq₁ : a₁ = a₁), eq.rec_on eq₁ b₁ = b₁ → P),
h rfl rfl),
eq.rec_on H₁₂ aux H₁₂