Zulip Chat Archive

Stream: new members

Topic: Getting a hypothesis that agrees with the match branch


Eric Wieser (Dec 13 2020 at 12:49):

I'm stuck o n the first sorry here - my goal is exactly the description of the match branch I'm in, but I don't appear to have a proof to hand:

import group_theory.perm.subgroup

def inv_sum_congr {ιa ιb : Type*} (σ : equiv.perm.sum_congr_subgroup ιa ιb) : equiv.perm ιa :=
{ to_fun := λ i, match σ (sum.inl i) with
  | (sum.inl il) := il
  | (sum.inr ir) := false.elim begin
      obtain σ, sl, sr, h := σ,
      replace h := _root_.congr_arg (λ σ : equiv.perm _, σ (sum.inl i)) h,
      simp at h,
      have h2 : sum.inl (sl i)  (sum.inr ir) := by simp only [ne.def, not_false_iff],
      apply h2,
      rw h,
      --`⊢ ⇑σ (sum.inl i) = sum.inr ir` ir is exactly our match condition!
      sorry
    end
  end,
  inv_fun := sorry,
  left_inv := sorry,
  right_inv := sorry}

Eric Wieser (Dec 13 2020 at 13:00):

I can get there with

def with_proof {α : Type*} (a : α) : {a' : α // a = a'} := a, rfl

and thenusing match with_proof (σ (sum.inl i)) with .... Does with_proof exist as a syntax feature already?

Bryan Gin-ge Chen (Dec 13 2020 at 13:17):

Every once in a while something like this gets asked and Mario usually pops up with some solution that uses match _, rfl : \forall, e.g. 1 2 3

Eric Wieser (Dec 13 2020 at 13:32):

Thanks, that solves my need for with_proof, but I still get stuck trying to unfold the matches

Eric Wieser (Dec 13 2020 at 13:36):

I get stuck here:

def inv_sum_congr {ιa ιb : Type*} (σ : equiv.perm.sum_congr_subgroup ιa ιb) : equiv.perm ιa :=
{ to_fun := λ i, match _, rfl :  x, x = σ.1 (sum.inl i)  _ with
  | (sum.inl il), _ := il
  | (sum.inr ir), h := false.elim $ let sl, sr, h2 := σ.2 in by simpa [h2] using h
  end,
  inv_fun := λ i, match _, rfl :  x, x = σ⁻¹.1 (sum.inl i)  _ with
  | (sum.inl il), _ := il
  | (sum.inr ir), h := false.elim $ let sl, sr, h2 := σ⁻¹.2 in by simpa [h2] using h
  end,
  left_inv := λ i, match _, rfl :  x, x = σ.1 (sum.inl i)  _ with
  | (sum.inl il), h := begin
      simp only,
      simp_rw h,
      sorry
    end
  | (sum.inr ir), h := false.elim $ let sl, sr, h2 := σ.2 in by simpa [h2] using h
  end,
  right_inv := λ i, sorry}

Mario Carneiro (Dec 13 2020 at 14:17):

I think the better solution is just to go to tactic mode and use cases e : x which handles this

Mario Carneiro (Dec 13 2020 at 14:17):

I haven't needed to write match x, rfl : ... since that was added

Eric Wieser (Dec 13 2020 at 14:19):

Oh true, tactic mode would be fine in the two proof fields

Eric Wieser (Dec 13 2020 at 14:20):

Would tactic mode be a bad idea for the data fields?

Mario Carneiro (Dec 13 2020 at 14:21):

It's fine as long as you are aware what all the tactics you use desugar to

Mario Carneiro (Dec 13 2020 at 14:21):

This kind of construction is difficult to work with regardless of how you write it

Mario Carneiro (Dec 13 2020 at 14:22):

because you have to induct over the x and rfl simultaneously in order to unfold the match, and this involves some messy dependent inductive hypothesis

Mario Carneiro (Dec 13 2020 at 14:26):

I think those matches should actually be a function on their own, like sum.resolve_left : \all x: A + B, (\ex y, x = sum.inl y) -> A

Eric Wieser (Dec 13 2020 at 14:27):

I was thinking about that too

Eric Wieser (Dec 13 2020 at 14:28):

Is there a more generic version of that to non-classically unpack an exists of an inductive type?

Mario Carneiro (Dec 13 2020 at 14:28):

it would be even better if such functions were generated automatically because they work for all inductive types

Eric Wieser (Dec 13 2020 at 14:28):

Or is a type like sum.elim (fun _, true) (fun _, false) a better thing to use as an argument than exists?

Mario Carneiro (Dec 13 2020 at 14:30):

I have considered the following scheme: T.discr : T -> nat returns the discriminant, i.e. 0 for the first case, 1 for the second, etc, and T.extract_c : \all x : T, x.discr = n -> A x B gets case | c : A -> B -> T with discriminant n

Mario Carneiro (Dec 13 2020 at 14:31):

Alternatively, extract_c can return option (A x B) and there are theorems about what its is_some looks like so you can use option.get

Mario Carneiro (Dec 13 2020 at 14:32):

The cool thing is that this represents the primitive operations of the VM, so they have efficient implementations even better than match

Eric Wieser (Dec 13 2020 at 14:34):

extract_c could go with -> \sigma a b, x = c a b right?

Mario Carneiro (Dec 13 2020 at 14:34):

Also, for very large inductive types, this scheme is asymptotically better than the standard O(n^2) decidable_eq implementation

Mario Carneiro (Dec 13 2020 at 14:35):

It could also be broken into a bunch of functions instead of a pair- or sigma- returning function

Mario Carneiro (Dec 13 2020 at 14:36):

the equality would be a theorem, there's no need to pack it in the return value

Yakov Pechersky (Dec 13 2020 at 16:24):

I've been having similar issues with casing on inductive types. What would be the main expected challenge in generating such functions for all inductive types?

Eric Wieser (Dec 13 2020 at 16:53):

Packing it in the return value seems like an easy way to generalize over arbitrary telescopes

Eric Wieser (Dec 13 2020 at 16:53):

Rather that having a special case for the last argument which doesn't get a binder


Last updated: Dec 20 2023 at 11:08 UTC