Getting a hypothesis that agrees with the match branch

Stream: new members

[Eric Wieser]

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]

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]

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]

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

[Eric Wieser]

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]

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

[Mario Carneiro]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

I was thinking about that too

[Eric Wieser]

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

[Mario Carneiro]

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

[Eric Wieser]

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

[Mario Carneiro]

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]

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]

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

[Eric Wieser]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Yakov Pechersky]

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]

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

[Eric Wieser]

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