## 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,
}
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