feat(frontends/lean): change notation for inaccessible patterns
The following are accepted .(t) ._ We don't accept .t anymore because it will conflict with the field access notation.
This commit is contained in:
Leonardo de Moura
parent
6183c7676e
commit
87932f1c56
41 changed files with 123 additions and 118 deletions
|
|
@ -90,7 +90,7 @@ section accum
|
|||
end accum
|
||||
|
||||
protected lemma eq {n : ℕ} : ∀ (a1 a2 : vector α n), to_list a1 = to_list a2 → a1 = a2
|
||||
| ⟨x, h1⟩ ⟨.x, h2⟩ rfl := rfl
|
||||
| ⟨x, h1⟩ ⟨._, h2⟩ rfl := rfl
|
||||
|
||||
@[simp] lemma to_list_mk (v : list α) (P : list.length v = n) : to_list (subtype.mk v P) = v :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -16,10 +16,10 @@ def {u} elim0 {α : Type u} : fin 0 → α
|
|||
variable {n : nat}
|
||||
|
||||
lemma eq_of_veq : ∀ {i j : fin n}, (val i) = (val j) → i = j
|
||||
| ⟨iv, ilt₁⟩ ⟨.iv, ilt₂⟩ rfl := rfl
|
||||
| ⟨iv, ilt₁⟩ ⟨.(iv), ilt₂⟩ rfl := rfl
|
||||
|
||||
lemma veq_of_eq : ∀ {i j : fin n}, i = j → (val i) = (val j)
|
||||
| ⟨iv, ilt⟩ .⟨iv, ilt⟩ rfl := rfl
|
||||
| ⟨iv, ilt⟩ .(_) rfl := rfl
|
||||
|
||||
lemma ne_of_vne {i j : fin n} (h : val i ≠ val j) : i ≠ j :=
|
||||
λ h', absurd (veq_of_eq h') h
|
||||
|
|
|
|||
|
|
@ -287,8 +287,8 @@ lemma le_add_left (n m : ℕ): n ≤ m + n :=
|
|||
nat.add_comm n m ▸ le_add_right n m
|
||||
|
||||
lemma le.dest : ∀ {n m : ℕ}, n ≤ m → ∃ k, n + k = m
|
||||
| n .n (less_than_or_equal.refl .n) := ⟨0, rfl⟩
|
||||
| n .(succ m) (@less_than_or_equal.step .n m h) :=
|
||||
| n ._ (less_than_or_equal.refl ._) := ⟨0, rfl⟩
|
||||
| n ._ (@less_than_or_equal.step ._ m h) :=
|
||||
match le.dest h with
|
||||
| ⟨w, hw⟩ := ⟨succ w, hw ▸ add_succ n w⟩
|
||||
end
|
||||
|
|
|
|||
|
|
@ -18,12 +18,12 @@ section
|
|||
variables {α : Type u} {β : α → Type v}
|
||||
|
||||
protected lemma sigma.eq : ∀ {p₁ p₂ : Σ a : α, β a} (h₁ : p₁.1 = p₂.1), (eq.rec_on h₁ p₁.2 : β p₂.1) = p₂.2 → p₁ = p₂
|
||||
| ⟨a, b⟩ ⟨.a, .b⟩ rfl rfl := rfl
|
||||
| ⟨a, b⟩ ⟨.(a), .(b)⟩ rfl rfl := rfl
|
||||
end
|
||||
|
||||
section
|
||||
variables {α : Sort u} {β : α → Sort v}
|
||||
|
||||
protected lemma psigma.eq : ∀ {p₁ p₂ : psigma β} (h₁ : p₁.1 = p₂.1), (eq.rec_on h₁ p₁.2 : β p₂.1) = p₂.2 → p₁ = p₂
|
||||
| ⟨a, b⟩ ⟨.a, .b⟩ rfl rfl := rfl
|
||||
| ⟨a, b⟩ ⟨.(a), .(b)⟩ rfl rfl := rfl
|
||||
end
|
||||
|
|
|
|||
|
|
@ -20,7 +20,7 @@ lemma tag_irrelevant {a : α} (h1 h2 : p a) : mk a h1 = mk a h2 :=
|
|||
rfl
|
||||
|
||||
protected lemma eq : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
|
||||
| ⟨x, h1⟩ ⟨.x, h2⟩ rfl := rfl
|
||||
| ⟨x, h1⟩ ⟨.(x), h2⟩ rfl := rfl
|
||||
|
||||
end subtype
|
||||
|
||||
|
|
|
|||
|
|
@ -163,13 +163,13 @@ heq.rec_on h (eq.refl α)
|
|||
end
|
||||
|
||||
lemma eq_rec_heq {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} (h : a = a') (p : φ a), (eq.rec_on h p : φ a') == p
|
||||
| a .a rfl p := heq.refl p
|
||||
| a ._ rfl p := heq.refl p
|
||||
|
||||
lemma heq_of_eq_rec_left {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a = a') (h₂ : (eq.rec_on e p₁ : φ a') = p₂), p₁ == p₂
|
||||
| a .a p₁ p₂ (eq.refl .a) h := eq.rec_on h (heq.refl p₁)
|
||||
| a ._ p₁ p₂ (eq.refl ._) h := eq.rec_on h (heq.refl p₁)
|
||||
|
||||
lemma heq_of_eq_rec_right {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a' = a) (h₂ : p₁ = eq.rec_on e p₂), p₁ == p₂
|
||||
| a .a p₁ p₂ (eq.refl .a) h :=
|
||||
| a ._ p₁ p₂ (eq.refl ._) h :=
|
||||
have p₁ = p₂, from h,
|
||||
this ▸ heq.refl p₁
|
||||
|
||||
|
|
@ -177,19 +177,19 @@ lemma of_heq_true {a : Prop} (h : a == true) : a :=
|
|||
of_eq_true (eq_of_heq h)
|
||||
|
||||
lemma eq_rec_compose : ∀ {α β φ : Sort u} (p₁ : β = φ) (p₂ : α = β) (a : α), (eq.rec_on p₁ (eq.rec_on p₂ a : β) : φ) = eq.rec_on (eq.trans p₂ p₁) a
|
||||
| α .α .α (eq.refl .α) (eq.refl .α) a := rfl
|
||||
| α ._ ._ (eq.refl ._) (eq.refl ._) a := rfl
|
||||
|
||||
lemma eq_rec_eq_eq_rec : ∀ {α₁ α₂ : Sort u} {p : α₁ = α₂} {a₁ : α₁} {a₂ : α₂}, (eq.rec_on p a₁ : α₂) = a₂ → a₁ = eq.rec_on (eq.symm p) a₂
|
||||
| α .α rfl a .a rfl := rfl
|
||||
| α ._ rfl a ._ rfl := rfl
|
||||
|
||||
lemma eq_rec_of_heq_left : ∀ {α₁ α₂ : Sort u} {a₁ : α₁} {a₂ : α₂} (h : a₁ == a₂), (eq.rec_on (type_eq_of_heq h) a₁ : α₂) = a₂
|
||||
| α .α a .a (heq.refl .a) := rfl
|
||||
| α ._ a ._ (heq.refl ._) := rfl
|
||||
|
||||
lemma eq_rec_of_heq_right {α₁ α₂ : Sort u} {a₁ : α₁} {a₂ : α₂} (h : a₁ == a₂) : a₁ = eq.rec_on (eq.symm (type_eq_of_heq h)) a₂ :=
|
||||
eq_rec_eq_eq_rec (eq_rec_of_heq_left h)
|
||||
|
||||
lemma cast_heq : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a == a
|
||||
| α .α (eq.refl .α) a := heq.refl a
|
||||
| α ._ (eq.refl ._) a := heq.refl a
|
||||
|
||||
/- and -/
|
||||
|
||||
|
|
|
|||
|
|
@ -20,7 +20,7 @@ variables [has_to_string α]
|
|||
|
||||
protected meta def exceptional.to_string : exceptional α → string
|
||||
| (success a) := to_string a
|
||||
| (exception .α e) := "Exception: " ++ to_string (e options.mk)
|
||||
| (exception .(α) e) := "Exception: " ++ to_string (e options.mk)
|
||||
|
||||
meta instance : has_to_string (exceptional α) :=
|
||||
has_to_string.mk exceptional.to_string
|
||||
|
|
@ -31,11 +31,11 @@ variables {α β : Type}
|
|||
|
||||
protected meta def to_bool : exceptional α → bool
|
||||
| (success _) := tt
|
||||
| (exception .α _) := ff
|
||||
| (exception .(α) _) := ff
|
||||
|
||||
protected meta def to_option : exceptional α → option α
|
||||
| (success a) := some a
|
||||
| (exception .α _) := none
|
||||
| (exception .(α) _) := none
|
||||
|
||||
@[inline] protected meta def bind (e₁ : exceptional α) (e₂ : α → exceptional β) : exceptional β :=
|
||||
exceptional.cases_on e₁
|
||||
|
|
|
|||
|
|
@ -140,7 +140,7 @@ do o ← get_options,
|
|||
meta def returnex {α : Type} (e : exceptional α) : tactic α :=
|
||||
λ s, match e with
|
||||
| exceptional.success a := success a s
|
||||
| exceptional.exception .α f :=
|
||||
| exceptional.exception ._ f :=
|
||||
match get_options s with
|
||||
| success opt _ := exception (some (λ u, f opt)) none s
|
||||
| exception _ _ _ := exception (some (λ u, f options.mk)) none s
|
||||
|
|
|
|||
|
|
@ -951,6 +951,20 @@ static expr parse_lambda_cons(parser_state & p, unsigned, expr const *, pos_info
|
|||
return p.save_pos(mk_choice(cs.size(), cs.data()), pos);
|
||||
}
|
||||
|
||||
static expr parse_inaccessible(parser_state & p, unsigned, expr const *, pos_info const & pos) {
|
||||
if (!p.in_pattern())
|
||||
throw parser_error("inaccesible pattern notation `.(t)` can only be used in patterns", pos);
|
||||
expr e = p.parse_expr();
|
||||
p.check_token_next(get_rparen_tk(), "invalid inaccesible pattern, `)` expected");
|
||||
return p.save_pos(mk_inaccessible(e), pos);
|
||||
}
|
||||
|
||||
static expr parse_atomic_inaccessible(parser_state & p, unsigned, expr const *, pos_info const & pos) {
|
||||
if (!p.in_pattern())
|
||||
throw parser_error("inaccesible pattern notation `._` can only be used in patterns", pos);
|
||||
return p.save_pos(mk_inaccessible(p.save_pos(mk_expr_placeholder(), pos)), pos);
|
||||
}
|
||||
|
||||
parse_table init_nud_table() {
|
||||
action Expr(mk_expr_action());
|
||||
action Skip(mk_skip_action());
|
||||
|
|
@ -966,6 +980,8 @@ parse_table init_nud_table() {
|
|||
r = r.add({transition("(", mk_ext_action(parse_lparen))}, x0);
|
||||
r = r.add({transition("⟨", mk_ext_action(parse_constructor))}, x0);
|
||||
r = r.add({transition("{", mk_ext_action(parse_curly_bracket))}, x0);
|
||||
r = r.add({transition(".(", mk_ext_action(parse_inaccessible))}, x0);
|
||||
r = r.add({transition("._", mk_ext_action(parse_atomic_inaccessible))}, x0);
|
||||
r = r.add({transition("`(", mk_ext_action(parse_lazy_quoted_pexpr))}, x0);
|
||||
r = r.add({transition("``(", mk_ext_action(parse_quoted_pexpr))}, x0);
|
||||
r = r.add({transition("```(", mk_ext_action(parse_quoted_expr))}, x0);
|
||||
|
|
|
|||
|
|
@ -1949,9 +1949,7 @@ expr parser::parse_char_expr() {
|
|||
expr parser::parse_nud() {
|
||||
switch (curr()) {
|
||||
case token_kind::Keyword:
|
||||
if (m_in_pattern && curr_is_token(get_period_tk()))
|
||||
return parse_inaccessible();
|
||||
else if (curr_is_token(get_placeholder_tk()))
|
||||
if (curr_is_token(get_placeholder_tk()))
|
||||
return parse_placeholder();
|
||||
else
|
||||
return parse_nud_notation();
|
||||
|
|
@ -1998,10 +1996,7 @@ expr parser::parse_led(expr left) {
|
|||
unsigned parser::curr_lbp() const {
|
||||
switch (curr()) {
|
||||
case token_kind::Keyword:
|
||||
if (m_in_pattern && curr_is_token(get_period_tk()))
|
||||
return get_max_prec();
|
||||
else
|
||||
return get_token_info().expr_precedence();
|
||||
return get_token_info().expr_precedence();
|
||||
case token_kind::CommandKeyword: case token_kind::Eof:
|
||||
case token_kind::QuotedSymbol: case token_kind::DocBlock:
|
||||
case token_kind::ModDocBlock:
|
||||
|
|
|
|||
|
|
@ -87,7 +87,7 @@ void init_token_table(token_table & t) {
|
|||
{"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
|
||||
{"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0},
|
||||
{"Type", g_max_prec}, {"Type*", g_max_prec}, {"Sort", g_max_prec}, {"Sort*", g_max_prec},
|
||||
{"(:", g_max_prec}, {":)", 0},
|
||||
{"(:", g_max_prec}, {":)", 0}, {".(", g_max_prec}, {"._", g_max_prec},
|
||||
{"⟨", g_max_prec}, {"⟩", 0}, {"^", 0},
|
||||
{"//", 0}, {"|", 0}, {"with", 0}, {"without", 0}, {"...", 0}, {",", 0},
|
||||
{".", 0}, {":", 0}, {"!", 0}, {"calc", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", g_max_prec},
|
||||
|
|
|
|||
|
|
@ -1,9 +1,9 @@
|
|||
universe variables u
|
||||
definition f1 : nat → nat → nat
|
||||
| a .a := a
|
||||
| a .(a) := a
|
||||
|
||||
definition f2 : ∀ (a b c : nat), a = c → c = a
|
||||
| a b .b rfl := rfl
|
||||
| a b .(b) rfl := rfl
|
||||
|
||||
inductive vec (A : Type u) : nat → Type (max 1 u)
|
||||
| nil {} : vec 0
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
bad_inaccessible.lean:3:5: error: invalid use of inaccessible term, it is not fixed by other arguments
|
||||
bad_inaccessible.lean:6:7: error: invalid use of inaccessible term, the provided term is
|
||||
bad_inaccessible.lean:3:6: error: invalid use of inaccessible term, it is not fixed by other arguments
|
||||
bad_inaccessible.lean:6:8: error: invalid use of inaccessible term, the provided term is
|
||||
b
|
||||
but is expected to be
|
||||
a
|
||||
bad_inaccessible.lean:14:3: error: invalid use of inaccessible term, it is not completely fixed by other arguments
|
||||
bad_inaccessible.lean:14:2: error: invalid use of inaccessible term, it is not completely fixed by other arguments
|
||||
.?m_1 + 1
|
||||
|
|
|
|||
|
|
@ -27,5 +27,5 @@ variables f : A → A → A
|
|||
3- Produce a better error message.
|
||||
-/
|
||||
definition map_head : ∀ {n}, vec A n → vec A n → vec A n
|
||||
| .0 nil nil := nil
|
||||
| .(n+1) (@cons .A .n a va) (@cons .A n b vb) := cons (f a b) va
|
||||
| .(0) nil nil := nil
|
||||
| .(n+1) (@cons .(A) .(n) a va) (@cons .(A) n b vb) := cons (f a b) va
|
||||
|
|
|
|||
|
|
@ -5,5 +5,5 @@ term
|
|||
has type
|
||||
vec .?m_1 (n + 1)
|
||||
but is expected to have type
|
||||
vec A .(.?m_2 + 1)
|
||||
bad_inaccessible2.lean:31:46: error: ill-formed match/equations expression
|
||||
vec A . (.?m_2 + 1)
|
||||
bad_inaccessible2.lean:31:52: error: ill-formed match/equations expression
|
||||
|
|
|
|||
|
|
@ -12,6 +12,6 @@ variable (f : bool → bool → bool)
|
|||
|
||||
definition map2 : ∀ {n}, bv n → bv n → bv n
|
||||
| 0 nil nil := nil
|
||||
| (n+1) (cons .n b1 v1) (cons .n b2 v2) := cons n (f b1 b2) (map2 v1 v2)
|
||||
| (n+1) (cons .(n) b1 v1) (cons .(n) b2 v2) := cons n (f b1 b2) (map2 v1 v2)
|
||||
|
||||
#check map2.equations._eqn_2
|
||||
|
|
|
|||
|
|
@ -2,4 +2,4 @@ inductive R : ℕ → Prop
|
|||
| pos : ∀p n, R (p + n)
|
||||
|
||||
lemma R_id : ∀n, R n → R n
|
||||
| (.p + .n) (R.pos p n) := R.pos p n
|
||||
| (.(p) + .(n)) (R.pos p n) := R.pos p n
|
||||
|
|
|
|||
|
|
@ -1,3 +1,3 @@
|
|||
eqn_compiler_error_msg.lean:5:2: error: invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )')
|
||||
.p + .n
|
||||
eqn_compiler_error_msg.lean:5:24: error: ill-formed match/equations expression
|
||||
eqn_compiler_error_msg.lean:5:28: error: ill-formed match/equations expression
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ inductive imf {A : Type u} {B : Type v} (f : A → B) : B → Type (max 1 u v)
|
|||
| mk : ∀ (a : A), imf (f a)
|
||||
|
||||
definition inv_1 {A : Type u} {B : Type v} (f : A → B) : ∀ (b : B), imf f b → A
|
||||
| .(f a) (imf.mk .f a) := a
|
||||
| .(f a) (imf.mk .(f) a) := a
|
||||
|
||||
definition inv_2 {A : Type u} {B : Type v} (f : A → B) : ∀ (b : B), imf f b → A
|
||||
| ._ (imf.mk ._ a) := a
|
||||
|
|
@ -14,7 +14,7 @@ definition inv_3 {A : Type u} {B : Type v} (f : A → B) : ∀ (b : B), imf f b
|
|||
| .(f a) (mk a) := a -- Error, mk is not a constructor
|
||||
|
||||
definition inv_4 {A : Type u} {B : Type v} (f : A → B) : ∀ (b : B), imf f b → A
|
||||
| .(f a) (.mk a) := a -- Error, we cannot use inaccessible annotation around functions in applications
|
||||
| .(f a) (.(mk) a) := a -- Error, we cannot use inaccessible annotation around functions in applications
|
||||
|
||||
attribute [pattern] mk
|
||||
|
||||
|
|
@ -44,8 +44,8 @@ section
|
|||
open vec1
|
||||
|
||||
definition map_1 {A : Type u} (f : A → A → A) : Π {n}, vec1 A n → vec1 A n → vec1 A n
|
||||
| 0 (nil .A) (nil .A) := nil A
|
||||
| (n+1) (cons .n h₁ v₁) (cons .n h₂ v₂) := cons n (f h₁ h₂) (map_1 v₁ v₂)
|
||||
| 0 (nil .(A)) (nil .(A)) := nil A
|
||||
| (n+1) (cons .(n) h₁ v₁) (cons .(n) h₂ v₂) := cons n (f h₁ h₂) (map_1 v₁ v₂)
|
||||
|
||||
definition map_2 {A : Type u} (f : A → A → A) : Π {n}, vec1 A n → vec1 A n → vec1 A n
|
||||
| 0 (nil ._) (nil ._) := nil A
|
||||
|
|
@ -54,7 +54,7 @@ definition map_2 {A : Type u} (f : A → A → A) : Π {n}, vec1 A n → vec1 A
|
|||
/- In map_3, we use the inaccessible terms to avoid pattern/matching on the first argument -/
|
||||
definition map_3 {A : Type u} (f : A → A → A) : Π {n}, vec1 A n → vec1 A n → vec1 A n
|
||||
| ._ (nil ._) (nil ._) := nil A
|
||||
| ._ (cons n h₁ v₁) (cons .n h₂ v₂) := cons n (f h₁ h₂) (map_3 v₁ v₂)
|
||||
| ._ (cons n h₁ v₁) (cons .(n) h₂ v₂) := cons n (f h₁ h₂) (map_3 v₁ v₂)
|
||||
end
|
||||
|
||||
inductive vec2 (A : Type u) : nat → Type (max 1 u)
|
||||
|
|
@ -70,7 +70,7 @@ definition map_4 {A : Type u} (f : A → A → A) : Π {n}, vec2 A n → vec2 A
|
|||
|
||||
definition map_5 {A : Type u} (f : A → A → A) : Π {n}, vec2 A n → vec2 A n → vec2 A n
|
||||
| ._ nil nil := nil
|
||||
| ._ (@cons .A n h₁ v₁) (cons h₂ v₂) := cons (f h₁ h₂) (map_5 v₁ v₂)
|
||||
| ._ (@cons ._ n h₁ v₁) (cons h₂ v₂) := cons (f h₁ h₂) (map_5 v₁ v₂)
|
||||
|
||||
/-
|
||||
The following variant will be rejected by the new equation compiler.
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ inaccessible.lean:14:10: error: function expected at
|
|||
inaccessible.lean:14:2: error: invalid occurrence of macro expression in pattern (possible solution, mark term as inaccessible using '.( )')
|
||||
sorry
|
||||
inaccessible.lean:14:17: error: ill-formed match/equations expression
|
||||
inaccessible.lean:17:11: error: invalid inaccessible annotation, it cannot be used around functions in applications
|
||||
inaccessible.lean:17:12: error: invalid inaccessible annotation, it cannot be used around functions in applications
|
||||
inaccessible.lean:25:12: error: invalid pattern, 'a' already appeared in this pattern
|
||||
inaccessible.lean:28:3: error: function expected at
|
||||
f
|
||||
|
|
@ -17,5 +17,5 @@ but is expected to have type
|
|||
imf f sorry
|
||||
inaccessible.lean:28:16: error: ill-formed match/equations expression
|
||||
inaccessible.lean:31:4: error: invalid pattern, 'a' already appeared in this pattern
|
||||
inaccessible.lean:82:3: error: invalid use of inaccessible term, it is not completely fixed by other arguments
|
||||
inaccessible.lean:82:2: error: invalid use of inaccessible term, it is not completely fixed by other arguments
|
||||
.?m_1 + 1
|
||||
|
|
|
|||
|
|
@ -2,13 +2,13 @@ inductive imf {A B : Sort*} (f : A → B) : B → Sort*
|
|||
| mk : ∀ (a : A), imf (f a)
|
||||
|
||||
definition inv_1 {A B : Sort*} (f : A → B) : ∀ (b : B), imf f b → A
|
||||
| .(f .a) (imf.mk .f a) := a -- Error inaccessible annotation inside inaccessible annotation
|
||||
| .(f .(a)) (imf.mk .(f) a) := a -- Error inaccessible annotation inside inaccessible annotation
|
||||
|
||||
definition inv_2 {A B : Sort*} (f : A → B) : ∀ (b : B), imf f b → A
|
||||
| .(f a) (let x := (imf.mk .f a) in x) := a -- Error invalid occurrence of 'let' expression
|
||||
| .(f a) (let x := (imf.mk .(f) a) in x) := a -- Error invalid occurrence of 'let' expression
|
||||
|
||||
definition inv_3 {A B : Sort*} (f : A → B) : ∀ (b : B), imf f b → A
|
||||
| .(f a) ((λ (x : imf f b), x) (imf.mk .f a)) := a -- Error invalid occurrence of 'lambda' expression
|
||||
| .(f a) ((λ (x : imf f b), x) (imf.mk .(f) a)) := a -- Error invalid occurrence of 'lambda' expression
|
||||
|
||||
definition symm {A : Sort*} : ∀ a b : A, a = b → b = a
|
||||
| .a .a (eq.refl a) := rfl -- Error `a` in eq.refl must be marked as inaccessible since it is an inductive datatype parameter
|
||||
| .(a) .(a) (eq.refl a) := rfl -- Error `a` in eq.refl must be marked as inaccessible since it is an inductive datatype parameter
|
||||
|
|
|
|||
|
|
@ -1,9 +1,9 @@
|
|||
inaccessible2.lean:5:7: error: invalid occurrence of 'inaccessible' annotation, it must only occur in patterns
|
||||
inaccessible2.lean:5:8: error: invalid occurrence of 'inaccessible' annotation, it must only occur in patterns
|
||||
inaccessible2.lean:5:4: error: invalid use of inaccessible term, the provided term is
|
||||
f sorry
|
||||
but is expected to be
|
||||
f a
|
||||
inaccessible2.lean:8:10: error: invalid pattern, must be an application, constant, variable, type ascription or inaccessible term
|
||||
inaccessible2.lean:11:39: error: invalid expression, `)` expected
|
||||
inaccessible2.lean:14:9: error: invalid pattern, in a constructor application, the parameters of the inductive datatype must be marked as inaccessible
|
||||
inaccessible2.lean:14:20: error: ill-formed match/equations expression
|
||||
inaccessible2.lean:11:39: error: inaccesible pattern notation `.(t)` can only be used in patterns
|
||||
inaccessible2.lean:14:13: error: invalid pattern, in a constructor application, the parameters of the inductive datatype must be marked as inaccessible
|
||||
inaccessible2.lean:14:24: error: ill-formed match/equations expression
|
||||
|
|
|
|||
|
|
@ -3,5 +3,5 @@ inductive {u} Foo : Type → Type (u+1)
|
|||
| wrap : Π (X : Type), Foo X → Foo X
|
||||
|
||||
def rig : Π {X : Type}, Foo X → Foo X
|
||||
| X (Foo.wrap .X foo) := foo
|
||||
| X foo := foo
|
||||
| X (Foo.wrap .(X) foo) := foo
|
||||
| X foo := foo
|
||||
|
|
|
|||
|
|
@ -16,8 +16,8 @@ def get₂b {A : Type} : Π {n : ℕ}, Vec A (n+2) → A
|
|||
| n (cons x₁ (cons x₂ xs)) := x₂
|
||||
|
||||
def get₂c {A : Type} : Π {n : ℕ}, Vec A (n+2) → A
|
||||
| .n (@cons .A x₁ .(n+1) (@cons .A x₂ n xs)) := x₂
|
||||
| .(n) (@cons .(A) x₁ .(n+1) (@cons .(A) x₂ n xs)) := x₂
|
||||
|
||||
def get₂d {A : Type} : Π {n : ℕ}, Vec A (n+2) → A
|
||||
| .n (@cons .A x₁ (n+1) (@cons .A x₂ .n xs)) := x₂
|
||||
| .(n) (@cons .(A) x₁ (n+1) (@cons .(A) x₂ .(n) xs)) := x₂
|
||||
end Vec
|
||||
|
|
|
|||
|
|
@ -28,8 +28,8 @@ definition count_vars : Π {t : type}, @term (λ x, unit) t -> nat
|
|||
| Nat (Const x) := 0
|
||||
| Nat (Plus e1 e2) := count_vars e1 + count_vars e2
|
||||
| (Func A B) (Abs e1) := count_vars (e1 star)
|
||||
| B (@App ._ A .B e1 e2) := count_vars e1 + count_vars e2
|
||||
| B (@Let ._ A .B e1 e2) := count_vars e1 + count_vars (e2 star)
|
||||
| B (@App ._ A .(B) e1 e2) := count_vars e1 + count_vars e2
|
||||
| B (@Let ._ A .(B) e1 e2) := count_vars e1 + count_vars (e2 star)
|
||||
|
||||
definition var (t : type) : @term (λ x, unit) t :=
|
||||
Var star
|
||||
|
|
|
|||
|
|
@ -1,2 +1,2 @@
|
|||
theorem cast_heq₂ : ∀ {A B : Type} (H : A = B) (a : A), cast H a == a
|
||||
| A .A (eq.refl .A) a := heq_of_eq $ cast_eq _ _
|
||||
| A .(A) (eq.refl .(A)) a := heq_of_eq $ cast_eq _ _
|
||||
|
|
|
|||
|
|
@ -1,3 +1,2 @@
|
|||
|
||||
theorem ex {A : Type} : ∀ {a a' : A}, a == a' → a = a'
|
||||
| a .a (heq.refl .a) := eq.refl a
|
||||
| a .(a) (heq.refl .(a)) := eq.refl a
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@ open bv bool
|
|||
|
||||
definition h : ∀ {n}, bv (succ (succ n)) → bool
|
||||
| .(succ m) (cons (succ (succ m)) b v) := b
|
||||
| .0 (cons (succ nat.zero) b v) := bnot b
|
||||
| .(0) (cons (succ nat.zero) b v) := bnot b
|
||||
|
||||
example (m : nat) (b : bool) (v : bv (succ (succ m))) : @h (succ m) (cons (succ (succ m)) b v) = b :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -1,4 +1,3 @@
|
|||
|
||||
inductive vec (A : Type) : nat → Type
|
||||
| nil {} : vec 0
|
||||
| cons : Π {n}, A → vec n → vec (n+1)
|
||||
|
|
@ -9,8 +8,8 @@ variables {A : Type}
|
|||
variables f : A → A → A
|
||||
|
||||
definition map_head_1 : ∀ {n}, vec A n → vec A n → vec A n
|
||||
| .0 nil nil := nil
|
||||
| .(n+1) (@cons .A n a va) (cons b vb) := cons (f a b) va
|
||||
| .(0) nil nil := nil
|
||||
| .(n+1) (@cons .(A) n a va) (cons b vb) := cons (f a b) va
|
||||
|
||||
example : map_head_1 f nil nil = nil :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -1,9 +1,8 @@
|
|||
|
||||
inductive imf {A B : Type} (f : A → B) : B → Type
|
||||
| mk : ∀ (a : A), imf (f a)
|
||||
|
||||
definition g {A B : Type} {f : A → B} : ∀ {b : B}, imf f b → A
|
||||
| .(f a) (imf.mk .f a) := a
|
||||
| .(f a) (imf.mk .(f) a) := a
|
||||
|
||||
example {A B : Type} (f : A → B) (a : A) : g (imf.mk f a) = a :=
|
||||
rfl
|
||||
|
|
@ -21,10 +20,10 @@ example : g v₂ = 0 :=
|
|||
rfl
|
||||
|
||||
lemma ex1 (A : Type) : ∀ (a b : A) (H : a = b), b = a
|
||||
| a .a rfl := rfl
|
||||
| a .(a) rfl := rfl
|
||||
|
||||
lemma ex2 (A : Type) : ∀ a b : A, a = b → b = a
|
||||
| a .a (eq.refl .a) := rfl
|
||||
| a .(a) (eq.refl .(a)) := rfl
|
||||
|
||||
lemma ex3 (A : Type) : ∀ a b : A, a = b → b = a
|
||||
| a ._ (eq.refl ._) := rfl
|
||||
|
|
|
|||
|
|
@ -1,3 +1,2 @@
|
|||
|
||||
lemma ex4 (A : Type) : ∀ (a b : A) (H : a = b), b = a
|
||||
| .z z (eq.refl .z) := eq.refl z
|
||||
| .(z) z (eq.refl .(z)) := eq.refl z
|
||||
|
|
|
|||
|
|
@ -1,4 +1,3 @@
|
|||
|
||||
inductive foo : bool → Type
|
||||
| Z : foo ff
|
||||
| O : foo ff → foo tt
|
||||
|
|
@ -7,9 +6,9 @@ inductive foo : bool → Type
|
|||
open foo
|
||||
|
||||
definition to_nat : ∀ {b}, foo b → nat
|
||||
| .ff Z := 0
|
||||
| .tt (O n) := to_nat n + 1
|
||||
| .ff (E n) := to_nat n + 1
|
||||
| .(ff) Z := 0
|
||||
| .(tt) (O n) := to_nat n + 1
|
||||
| .(ff) (E n) := to_nat n + 1
|
||||
|
||||
example : to_nat (E (O Z)) = 2 :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -9,8 +9,8 @@ open bv
|
|||
variable (f : bool → bool → bool)
|
||||
|
||||
definition map2 : ∀ {n}, bv n → bv n → bv n
|
||||
| .0 nil nil := nil
|
||||
| .(n+1) (cons n b1 v1) (cons .n b2 v2) := cons n (f b1 b2) (map2 v1 v2)
|
||||
| .(0) nil nil := nil
|
||||
| .(n+1) (cons n b1 v1) (cons .(n) b2 v2) := cons n (f b1 b2) (map2 v1 v2)
|
||||
|
||||
example : map2 f nil nil = nil :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ variable (f : bool → bool → bool)
|
|||
|
||||
definition map2 : ∀ {n}, bv n → bv n → bv n
|
||||
| 0 nil nil := nil
|
||||
| (n+1) (cons .n b1 v1) (cons .n b2 v2) := cons n (f b1 b2) (map2 v1 v2)
|
||||
| (n+1) (cons .(n) b1 v1) (cons .(n) b2 v2) := cons n (f b1 b2) (map2 v1 v2)
|
||||
|
||||
example : map2 f nil nil = nil :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -5,9 +5,9 @@ inductive bv : nat → Type
|
|||
open bv
|
||||
|
||||
definition f : ∀ n : nat, bv n → nat → nat
|
||||
| (n+1) (cons .n b v) 1000000 := f n v 0
|
||||
| (n+1) (cons .n b v) x := f n v (x + 1)
|
||||
| _ _ _ := 1
|
||||
| (n+1) (cons .(n) b v) 1000000 := f n v 0
|
||||
| (n+1) (cons .(n) b v) x := f n v (x + 1)
|
||||
| _ _ _ := 1
|
||||
|
||||
set_option pp.binder_types true
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,5 @@
|
|||
|
||||
definition symm {A : Type} : Π {a b : A}, a = b → b = a
|
||||
| a .a rfl := rfl
|
||||
| a .(a) rfl := rfl
|
||||
|
||||
definition trans {A : Type} : Π {a b c : A}, a = b → b = c → a = c
|
||||
| a .a .a rfl rfl := rfl
|
||||
| a .(a) .(a) rfl rfl := rfl
|
||||
|
|
|
|||
|
|
@ -3,5 +3,5 @@ attribute [pattern] lt.base
|
|||
attribute [pattern] lt.step
|
||||
|
||||
theorem lt_succ {a : nat} : ∀ {b : nat}, a < b → succ a < succ b
|
||||
| .(succ a) (lt.base .a) := lt.base (succ a)
|
||||
| .(succ b) (@lt.step .a b h) := lt.step (lt_succ h)
|
||||
| .(succ a) (lt.base .(a)) := lt.base (succ a)
|
||||
| .(succ b) (@lt.step .(a) b h) := lt.step (lt_succ h)
|
||||
|
|
|
|||
|
|
@ -3,5 +3,5 @@ inductive imf (f : nat → nat) : nat → Type
|
|||
| mk2 : imf (f 0 + 1)
|
||||
|
||||
definition inv_2 (f : nat → nat) : ∀ (b : nat), imf f b → {x : nat // x > b} → nat
|
||||
| .(f a) (imf.mk1 .f a) x := a
|
||||
| .(f 0 + 1) (imf.mk2 .f) x := subtype.val x
|
||||
| .(f a) (imf.mk1 .(f) a) x := a
|
||||
| .(f 0 + 1) (imf.mk2 .(f)) x := subtype.val x
|
||||
|
|
|
|||
|
|
@ -17,10 +17,10 @@ definition pack {A : Sort*} : list (tree A) → tree_core A tt
|
|||
| (a::l) := cons' a (pack l)
|
||||
|
||||
definition unpack {A : Sort*} : ∀ {b}, tree_core A b → list (tree A)
|
||||
| .tt nil' := []
|
||||
| .tt (cons' a t) := a :: unpack t
|
||||
| .ff (leaf' a) := []
|
||||
| .ff (node' l) := []
|
||||
| .(tt) nil' := []
|
||||
| .(tt) (cons' a t) := a :: unpack t
|
||||
| .(ff) (leaf' a) := []
|
||||
| .(ff) (node' l) := []
|
||||
|
||||
attribute [inverse]
|
||||
lemma unpack_pack {A : Sort*} : ∀ (l : list (tree A)), unpack (pack l) = l
|
||||
|
|
|
|||
|
|
@ -85,16 +85,16 @@ namespace PropF
|
|||
open Nc
|
||||
|
||||
lemma weakening2 : ∀ {Γ A Δ}, Γ ⊢ A → Γ ⊆ Δ → Δ ⊢ A
|
||||
| .Γ .A Δ (Nax Γ A Hin) Hs := Nax _ _ (Hs Hin)
|
||||
| .Γ .(A ⇒ B) Δ (ImpI Γ A B H) Hs := ImpI _ _ _ (weakening2 H (cons_subset_cons A Hs))
|
||||
| .Γ .B Δ (ImpE Γ A B H₁ H₂) Hs := ImpE _ _ _ (weakening2 H₁ Hs) (weakening2 H₂ Hs)
|
||||
| .Γ .A Δ (BotC Γ A H) Hs := BotC _ _ (weakening2 H (cons_subset_cons (~A) Hs))
|
||||
| .Γ .(A ∧ B) Δ (AndI Γ A B H₁ H₂) Hs := AndI _ _ _ (weakening2 H₁ Hs) (weakening2 H₂ Hs)
|
||||
| .Γ .A Δ (AndE₁ Γ A B H) Hs := AndE₁ _ _ _ (weakening2 H Hs)
|
||||
| .Γ .B Δ (AndE₂ Γ A B H) Hs := AndE₂ _ _ _ (weakening2 H Hs)
|
||||
| .Γ .(A ∨ B) Δ (OrI₁ Γ A B H) Hs := OrI₁ _ _ _ (weakening2 H Hs)
|
||||
| .Γ .(A ∨ B) Δ (OrI₂ Γ A B H) Hs := OrI₂ _ _ _ (weakening2 H Hs)
|
||||
| .Γ .C Δ (OrE Γ A B C H₁ H₂ H₃) Hs :=
|
||||
| ._ ._ Δ (Nax Γ A Hin) Hs := Nax _ _ (Hs Hin)
|
||||
| ._ .(A ⇒ B) Δ (ImpI Γ A B H) Hs := ImpI _ _ _ (weakening2 H (cons_subset_cons A Hs))
|
||||
| ._ ._ Δ (ImpE Γ A B H₁ H₂) Hs := ImpE _ _ _ (weakening2 H₁ Hs) (weakening2 H₂ Hs)
|
||||
| ._ ._ Δ (BotC Γ A H) Hs := BotC _ _ (weakening2 H (cons_subset_cons (~A) Hs))
|
||||
| ._ .(A ∧ B) Δ (AndI Γ A B H₁ H₂) Hs := AndI _ _ _ (weakening2 H₁ Hs) (weakening2 H₂ Hs)
|
||||
| ._ ._ Δ (AndE₁ Γ A B H) Hs := AndE₁ _ _ _ (weakening2 H Hs)
|
||||
| ._ ._ Δ (AndE₂ Γ A B H) Hs := AndE₂ _ _ _ (weakening2 H Hs)
|
||||
| ._ .(A ∨ B) Δ (OrI₁ Γ A B H) Hs := OrI₁ _ _ _ (weakening2 H Hs)
|
||||
| ._ .(A ∨ B) Δ (OrI₂ Γ A B H) Hs := OrI₂ _ _ _ (weakening2 H Hs)
|
||||
| ._ ._ Δ (OrE Γ A B C H₁ H₂ H₃) Hs :=
|
||||
OrE _ _ _ _ (weakening2 H₁ Hs) (weakening2 H₂ (cons_subset_cons A Hs)) (weakening2 H₃ (cons_subset_cons B Hs))
|
||||
|
||||
lemma weakening : ∀ Γ Δ A, Γ ⊢ A → Γ++Δ ⊢ A :=
|
||||
|
|
@ -117,8 +117,8 @@ namespace PropF
|
|||
attribute [simp] is_true TrueQ
|
||||
|
||||
theorem Soundness_general {v : valuation} : ∀ {A Γ}, Γ ⊢ A → Satisfies v Γ → is_true (TrueQ v A)
|
||||
| .A .Γ (Nax Γ A Hin) s := s _ Hin
|
||||
| .(A ⇒ B) .Γ (ImpI Γ A B H) s :=
|
||||
| ._ ._ (Nax Γ A Hin) s := s _ Hin
|
||||
| .(A ⇒ B) ._ (ImpI Γ A B H) s :=
|
||||
by_cases
|
||||
(λ t : is_true (TrueQ v A),
|
||||
have Satisfies v (A::Γ), from Satisfies_cons s t,
|
||||
|
|
@ -128,34 +128,34 @@ namespace PropF
|
|||
have TrueQ v A = ff, by simp at f; simph,
|
||||
have bnot (TrueQ v A) = tt, by simph,
|
||||
by simph)
|
||||
| .B .Γ (ImpE Γ A B H₁ H₂) s :=
|
||||
| ._ ._ (ImpE Γ A B H₁ H₂) s :=
|
||||
have aux : TrueQ v A = tt, from Soundness_general H₂ s,
|
||||
have bnot (TrueQ v A) || TrueQ v B = tt, from Soundness_general H₁ s,
|
||||
by simp [aux] at this; simph
|
||||
| .A .Γ (BotC Γ A H) s := by_contradiction
|
||||
| ._ ._ (BotC Γ A H) s := by_contradiction
|
||||
(λ n : TrueQ v A ≠ tt,
|
||||
have TrueQ v A = ff, by {simp at n; simph},
|
||||
have TrueQ v (~A) = tt, begin change (bnot (TrueQ v A) || ff = tt), simph end,
|
||||
have Satisfies v ((~A)::Γ), from Satisfies_cons s this,
|
||||
have TrueQ v ⊥ = tt, from Soundness_general H this,
|
||||
absurd this ff_ne_tt)
|
||||
| .(A ∧ B) .Γ (AndI Γ A B H₁ H₂) s :=
|
||||
| .(A ∧ B) ._ (AndI Γ A B H₁ H₂) s :=
|
||||
have TrueQ v A = tt, from Soundness_general H₁ s,
|
||||
have TrueQ v B = tt, from Soundness_general H₂ s,
|
||||
by simph
|
||||
| .A .Γ (AndE₁ Γ A B H) s :=
|
||||
| ._ ._ (AndE₁ Γ A B H) s :=
|
||||
have TrueQ v (A ∧ B) = tt, from Soundness_general H s,
|
||||
by simp [TrueQ] at this; simph [is_true]
|
||||
| .B .Γ (AndE₂ Γ A B H) s :=
|
||||
| ._ ._ (AndE₂ Γ A B H) s :=
|
||||
have TrueQ v (A ∧ B) = tt, from Soundness_general H s,
|
||||
by simp at this; simph
|
||||
| .(A ∨ B) .Γ (OrI₁ Γ A B H) s :=
|
||||
| .(A ∨ B) ._ (OrI₁ Γ A B H) s :=
|
||||
have TrueQ v A = tt, from Soundness_general H s,
|
||||
by simph
|
||||
| .(A ∨ B) .Γ (OrI₂ Γ A B H) s :=
|
||||
| .(A ∨ B) ._ (OrI₂ Γ A B H) s :=
|
||||
have TrueQ v B = tt, from Soundness_general H s,
|
||||
by simph
|
||||
| .C .Γ (OrE Γ A B C H₁ H₂ H₃) s :=
|
||||
| ._ ._ (OrE Γ A B C H₁ H₂ H₃) s :=
|
||||
have TrueQ v A || TrueQ v B = tt, from Soundness_general H₁ s,
|
||||
have or (TrueQ v A = tt) (TrueQ v B = tt), by simp at this; simph,
|
||||
or.elim this
|
||||
|
|
|
|||
|
|
@ -7,13 +7,13 @@ inductive ifin : ℕ → Type -- inductively defined fin-type
|
|||
open ifin
|
||||
|
||||
definition foo {N : Type} : Π{n : ℕ}, N → ifin n → (N × ifin n)
|
||||
| (succ k) n (fz .k) := sorry
|
||||
| (succ k) n (fz .(k)) := sorry
|
||||
| (succ k) n (fs x) := sorry
|
||||
|
||||
definition bar {N : Type} : Π{n : ℕ}, (N × ifin n) → (N × ifin n)
|
||||
| (succ k) (n, fz .k) := sorry
|
||||
| (succ k) (n, fz .(k)) := sorry
|
||||
| (succ k) (n, fs x) := sorry
|
||||
|
||||
definition bar2 {N : Type} : Π{n : ℕ}, (N × ifin n) → (N × ifin n)
|
||||
| (succ k) (n, fz .k) := sorry
|
||||
| (succ k) (n, fz .(k)) := sorry
|
||||
| (succ k) (n, fs x) := sorry
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue