9a41f0f899
Before this commit, the `by_cases p` tactic would synthesize
`inst : decidable p` type class resolution, and then use the
`cases` tactic (dependent elimination). This would create
problems since occurrences of `inst` would be replaced with
`decidable.is_true h` in one branch, and `decidable.is_false h` in the
other. Where `h`s (we have two of them, one for each branch) are
fresh hypotheses introduced by the `cases` tactic.
For example, assume we have the term in our goal.
`@ite p inst A a b`
This term would become
`@ite p (decidable.is_true h) A a b` (in the first branch where `h : p`)
and
`@ite p (decidable.is_false h) A a b` (in the second where `h : not p`)
Now, suppose we try to executed the following tactic in the first branch
`rw [if_pos h]`
it will fail since `if_pos h` is actually `@if_pos p inst h`, and
we will not be able to unify
`@ite p (decidable.is_true h) A a b =?= @ite p inst ?A ?a ?b`
This commit workarounds this problem by applying cases on
`@decidable.em p inst : p or not p` instead of `inst : decidable p`.
Thus, the term `inst` is not replaced with `decidable.is_true h` and
`decidable.is_false h`.
The new test `tests/lean/run/simp_dif.lean` demonstrates the problem above.
24 lines
1 KiB
Text
24 lines
1 KiB
Text
constant safe_div (a b : nat) : b ≠ 0 → nat
|
||
|
||
example (a b : nat) (h : ¬b ≠ 0) : (if h : b ≠ 0 then safe_div a b h else a) = a :=
|
||
by simp [dif_neg h]
|
||
example (a b : nat) (h : b ≠ 0) : (if h : b ≠ 0 then safe_div a b h else a) = safe_div a b h :=
|
||
by simp [dif_pos h]
|
||
example (a b : nat) (h : ¬b ≠ 0) : (if h : b ≠ 0 then safe_div a b h else a) = a :=
|
||
by rw [dif_neg h]
|
||
example (a b : nat) (h : b ≠ 0) : (if h : b ≠ 0 then safe_div a b h else a) = safe_div a b h :=
|
||
by rw [dif_pos h]
|
||
|
||
example (a b : nat) : (if h : b ≠ 0 then safe_div a b h else a) = a ∨ ∃ h, (if h : b ≠ 0 then safe_div a b h else a) = safe_div a b h :=
|
||
begin
|
||
by_cases (b ≠ 0),
|
||
{apply or.inr, rw [dif_pos h], existsi h, refl},
|
||
{apply or.inl, rw [dif_neg h]}
|
||
end
|
||
|
||
example (a b : nat) : (if h : b ≠ 0 then safe_div a b h else a) = a ∨ ∃ h, (if h : b ≠ 0 then safe_div a b h else a) = safe_div a b h :=
|
||
begin
|
||
by_cases (b ≠ 0),
|
||
{apply or.inr, simp [dif_pos h], existsi h, trivial},
|
||
{apply or.inl, simp [dif_neg h]}
|
||
end
|