# Zulip Chat Archive

## Stream: new members

### Topic: simp [dite_eq_ite] introduces quot.sound

#### Horatiu Cheval (Apr 14 2021 at 18:13):

I don't have a mwe because my question depends on quite a few definitions and I couldn't isolate it so far, but I think it's more of a general question, so I hope it's fine. I printed the axioms used by one of my proofs, and to my surpise I saw `quot.sound`

listed.

Then, by commenting out everything, I concluded that it is due to a `simp only [dite_eq_ite]`

. I can't understand why this happens, since `dite_eq_ite`

is proved just by `rfl`

(or maybe this doesn't have anything to do it). In any case, how can I understand why `quot.sound`

is used by simp?

#### Horatiu Cheval (Apr 14 2021 at 18:14):

And more generally, is there a more detailed way to track where the axioms of your proof, as listed by `#print axioms ...`

come from?

#### Kevin Buzzard (Apr 14 2021 at 18:17):

`#print axioms dite_eq_ite -- no axioms`

-- so your diagnosis is not correct and it's really hard to help you without a #mwe. Just post a large amount of code, maybe as a gist or whatever.

#### Alex J. Best (Apr 14 2021 at 18:23):

simp could be applying function extensionality https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#function-extensionality

#### Kevin Buzzard (Apr 14 2021 at 18:25):

```
example (α β : Type) (f g : α → β) : (∀ a, f a = g a) → f = g :=
begin
intro h,
simp [h], -- fails
end
```

I can't persuade `simp only`

to do this :-/

#### Kevin Buzzard (Apr 14 2021 at 18:27):

```
#print funext
/-
@[_ext_lemma_core, ext list.cons.{0} ext_param_type (sum.inr.{0 0} (option.{0} name) (option.{0} name) (option.some.{0} name (name.mk_numeral (unsigned.of_nat' (has_zero.zero.{0} nat nat.has_zero)) name.anonymous))) (list.cons.{0} ext_param_type (sum.inr.{0 0} (option.{0} name) (option.{0} name) (option.some.{0} name (name.mk_string "thunk" name.anonymous))) (list.nil.{0} ext_param_type)), intro!]
...
-/
```

It's outputs like that which remind me how little I know.

#### Horatiu Cheval (Apr 14 2021 at 18:30):

Ok, so I managed to reduce it to this (I don't think the decidability proof is relevant, but who knows, I included it nevertheless).

The proof I'm interested in is `and_contr`

```
import tactic
inductive formula : Type 1
| prime : Π (p : Prop) [decidable p], formula
| implication : formula → formula → formula
| conjunction : formula → formula → formula
namespace formula
infixr `⟹` : 45 := implication
infix `⋀` : 50 := conjunction
@[simp]
def mwc : formula → Type × Type
| (@prime _ _) := (unit, unit)
| (A ⋀ B) := (A.mwc.1 × B.mwc.1, A.mwc.2 × B.mwc.2)
| (A ⟹ B) := ((A.mwc.1 → B.mwc.2 → A.mwc.2) × ((A.mwc.1 → B.mwc.1)), A.mwc.1 × B.mwc.2)
@[reducible, simp]
def 𝕎 := λ A : formula, A.mwc.fst
@[reducible, simp]
def ℂ := λ A : formula, A.mwc.snd
def dia : Π A : formula, A.𝕎 → A.ℂ → Prop
| (@prime p _) x y := p
| (A ⋀ B) x y := (A.dia x.fst y.fst) ∧ (B.dia x.snd y.snd)
| (A ⟹ B) x y := (A.dia y.fst (x.fst y.fst y.snd)) → (B.dia (x.snd y.fst) y.snd)
instance dia.decidable (A : formula) (x : A.𝕎) (y : A.ℂ) : decidable $ A.dia x y :=
begin
induction A,
case prime
{ assumption, },
case conjunction: A B ihA ihB {
simp only [dia],
specialize ihA x.fst y.fst,
specialize ihB x.snd y.snd,
exact @and.decidable _ _ ihA ihB,
},
case implication: A B ihA ihB {
simp only [dia],
specialize ihA y.fst (x.fst y.fst y.snd),
specialize ihB (x.snd y.fst) y.snd,
refine @implies.decidable _ _ ihA ihB,
},
end
def sound (A : formula) := {t : A.𝕎 // ∀ y : ℂ A, A.dia t y}
def and_contr {A : formula} : sound (A ⟹ A ⋀ A) :=
begin
refine subtype.mk (by {
dsimp,
apply prod.mk,
{
intros x y,
by_cases h : A.dia x y.fst,
{
exact y.snd,
},
{
exact y.fst,
}
},
{
intros x,
exact (x, x),
}
}) _,
intros y,
simp only [dia, dite_eq_ite, id.def],
intros h,
dsimp only [mwc, ℂ] at y,
by_cases h' : A.dia y.fst y.snd.fst,
{
simp only [*, if_true] at h,
exact ⟨h', h⟩,
},
{
simp only [*, if_false] at h,
contradiction,
}
end
#print axioms and_contr
end formula
```

#### Mario Carneiro (Apr 14 2021 at 18:35):

Using `dsimp`

instead eliminates the use

#### Mario Carneiro (Apr 14 2021 at 18:35):

the reason `simp`

uses `quot.sound`

is because it is used in the proof of `funext`

which is needed for `simp`

to "rewrite under binders"

#### Mario Carneiro (Apr 14 2021 at 18:36):

`dsimp`

just needs lambda to respect defeq which doesn't require funext

#### Mario Carneiro (Apr 14 2021 at 18:38):

Kevin Buzzard said:

`#print funext /- @[_ext_lemma_core, ext list.cons.{0} ext_param_type (sum.inr.{0 0} (option.{0} name) (option.{0} name) (option.some.{0} name (name.mk_numeral (unsigned.of_nat' (has_zero.zero.{0} nat nat.has_zero)) name.anonymous))) (list.cons.{0} ext_param_type (sum.inr.{0 0} (option.{0} name) (option.{0} name) (option.some.{0} name (name.mk_string "thunk" name.anonymous))) (list.nil.{0} ext_param_type)), intro!] ... -/`

It's outputs like that which remind me how little I know.

Note that that mostly looks terrible only because lean doesn't use the pretty printer to show expressions in attributes like it should

#### Horatiu Cheval (Apr 14 2021 at 18:47):

I see, thanks for the clarifications!

Last updated: May 14 2021 at 13:24 UTC