simp [dite_eq_ite] introduces quot.sound

Stream: new members

[Horatiu Cheval]

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]

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]

#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]

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

[Kevin Buzzard]

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]

#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]

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]

Using dsimp instead eliminates the use

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

I see, thanks for the clarifications!