Zulip Chat Archive

Stream: new members

Topic: Rewriting hypotheses in (d)ites


view this post on Zulip Yakov Pechersky (Oct 01 2020 at 02:36):

What could be a short proof for this (and similar statements)?

lemma dif_symm {p q : Prop} {x y : } (h : dite (x = y) (λ _, p) (λ _, q)) :
  dite (y = x) (λ _, p) (λ _, q) := sorry

view this post on Zulip Yury G. Kudryashov (Oct 01 2020 at 02:57):

Use split_ifs?

view this post on Zulip Yury G. Kudryashov (Oct 01 2020 at 02:58):

In this particular case: by simpa [eq_comm]

view this post on Zulip Yakov Pechersky (Oct 01 2020 at 02:58):

Ah eq_comm is what I was looking for

view this post on Zulip Yury G. Kudryashov (Oct 01 2020 at 03:00):

There might be a problem if the types inside dite actually depend on the condition (or only for Type-values dites?)

view this post on Zulip Yury G. Kudryashov (Oct 01 2020 at 03:01):

I don't remember details.

view this post on Zulip Yury G. Kudryashov (Oct 01 2020 at 03:01):

In case of an error, I just use split_ifs

view this post on Zulip Yury G. Kudryashov (Oct 01 2020 at 03:01):

(or by_cases + simp [dif_pos ...])

view this post on Zulip Yakov Pechersky (Oct 01 2020 at 03:06):

The larger issue is that this is my goal after a wlog. I could for sure solve it without the wlog, but thought it'd be cleaner with.

      /-
R : Type u_1,
_inst_1 : field R,
n : ℕ,
A : matrix (fin (n + 3)) (fin (n + 3)) R,
x y : fin (n + 2 + 1),
H : y ≤ x,
this :
  dite (y = x) (λ (_x : y = x), 0)
      (λ (h : ¬y = x),
         -A 0 x * (-1) ^ ↑x * A 1 y * (-1) ^ ↑(x.pred_above y h) * det' ((A.drop 0 x).drop 0 (x.pred_above y h))) =
    dite (x = y) (λ (_x : x = y), 0)
      (λ (h : ¬x = y),
         A 1 y * (-1) ^ ↑y * A 0 x * (-1) ^ ↑(y.pred_above x h) * det' ((A.drop 0 y).drop 0 (y.pred_above x h)))
⊢ dite (x = y) (λ (_x : x = y), 0)
      (λ (h : ¬x = y),
         -A 0 y * (-1) ^ ↑y * A 1 x * (-1) ^ ↑(y.pred_above x h) * det' ((A.drop 0 y).drop 0 (y.pred_above x h))) =
    dite (y = x) (λ (_x : y = x), 0)
      (λ (h : ¬y = x),
         A 1 x * (-1) ^ ↑x * A 0 y * (-1) ^ ↑(x.pred_above y h) * det' ((A.drop 0 x).drop 0 (x.pred_above y h)))
-/

view this post on Zulip Yakov Pechersky (Oct 01 2020 at 03:07):

this is just the goal with the conditions reversed.

view this post on Zulip Yakov Pechersky (Oct 01 2020 at 03:07):

Almost.

view this post on Zulip Yakov Pechersky (Oct 01 2020 at 03:10):

I'll just go back to my wlog-free proof.


Last updated: May 09 2021 at 18:17 UTC