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

feat(library/definitional/equations): add support for reflexive datatypes in the definitional package

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-05 11:05:16 -08:00
parent 23fa16a23d
commit fdef3e5407
2 changed files with 47 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/library/definitional/equations.cpp
View file

@ -1101,8 +1101,11 @@ class equation_compiler_fn {
}
return none_expr();
} else if (is_pi(d)) {
// TODO(Leo)
return none_expr();
if (is_app(a)) {
return to_below(instantiate(binding_body(d), app_arg(a)), a, mk_app(b, app_arg(a)));
} else {
return none_expr();
}
} else {
return none_expr();
}

42
tests/lean/run/eq10.lean Normal file
View file

@ -0,0 +1,42 @@
inductive formula :=
eqf : nat → nat → formula,
andf : formula → formula → formula,
impf : formula → formula → formula,
notf : formula → formula,
orf : formula → formula → formula,
allf : (nat → formula) → formula
namespace formula
definition implies (a b : Prop) : Prop := a → b
definition denote : formula → Prop,
denote (eqf n1 n2) := n1 = n2,
denote (andf f1 f2) := denote f1 ∧ denote f2,
denote (impf f1 f2) := implies (denote f1) (denote f2),
denote (orf f1 f2) := denote f1 ∨ denote f2,
denote (notf f) := ¬ denote f,
denote (allf f) := ∀ n : nat, denote (f n)
theorem denote_eqf (n1 n2 : nat) : denote (eqf n1 n2) = (n1 = n2) :=
rfl
theorem denote_andf (f1 f2 : formula) : denote (andf f1 f2) = (denote f1 ∧ denote f2) :=
rfl
theorem denote_impf (f1 f2 : formula) : denote (impf f1 f2) = (denote f1 → denote f2) :=
rfl
theorem denote_orf (f1 f2 : formula) : denote (orf f1 f2) = (denote f1 ∨ denote f2) :=
rfl
theorem denote_notf (f : formula) : denote (notf f) = ¬ denote f :=
rfl
theorem denote_allf (f : nat → formula) : denote (allf f) = (∀ n, denote (f n)) :=
rfl
example : denote (allf (λ n₁, allf (λ n₂, impf (eqf n₁ n₂) (eqf n₂ n₁)))) =
(∀ n₁ n₂ : nat, n₁ = n₂ → n₂ = n₁) :=
rfl
end formula