Zulip Chat Archive

Stream: new members

Topic: simp [dite_eq_ite] introduces quot.sound


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 :-/

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 14 2021 at 18:35):

Using dsimp instead eliminates the use

view this post on Zulip 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"

view this post on Zulip Mario Carneiro (Apr 14 2021 at 18:36):

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

view this post on Zulip 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

view this post on Zulip Horatiu Cheval (Apr 14 2021 at 18:47):

I see, thanks for the clarifications!


Last updated: May 14 2021 at 13:24 UTC