Working around the elimination restriction

Stream: general

[Aaron Bies]

As part of a homework assignment, I wrote the following script in Coq:

Require Import Lia.
Notation "'sigma' x , B" := (sigT (fun x => B))
  (at level 200, right associativity).

Definition half' : forall x, sigma y, sum (2*y = x) (2*y = S x).
Proof.
  induction x as [| x [y [h|h]]].
  - exists 0. left. reflexivity.
  - exists (S y). right. lia.
  - exists y. left. exact h.
Defined.

Definition half (x : nat) : nat :=
  match (half' x) with existT _ y _ => y end.

Eval compute in half 6. (* This prints "3" *)

I tried to translate this into Lean, but I didn't get very far.

First, I tried it just it with ∃ and ∨, but this of course didn't make it past the elimination restriction.

def half_prop (x : ℕ) : ∃ y, 2 * y = x ∨ 2 * y = x + 1 :=
begin
  induction x with x ih,
  { use 0, left, refl, },

  rcases ih with ⟨y, h | h⟩,
  { use y + 1, right, rw ←h, refl, },
  { use y, left, exact h, },
end

def half (x : ℕ) : ℕ :=
begin
  cases half_prop x with y h, -- error, can only eliminate into Prop
  exact y,
end

Then, I tried using Σ and ⊕ to mirror how we got around the elimination restriction in Coq...

def half' (x : ℕ) : Σ y, (2 * y = x) ⊕ (2 * y = x + 1) :=
by sorry

...but this does not type check, because ⊕ does not accept Props as arguments.

Using Σ' I got further, but once again died to the elimination restriction.

def half' (x : ℕ) : Σ' y, (2 * y = x) ∨ (2 * y = x + 1) :=
begin
  induction x with x ih,
  { use 0, left, refl, },

  rcases ih with ⟨y, h | h⟩, -- can only eliminate into Prop
end

Does anyone know how can I get this to work?

[Junyan Xu]

Instead of ⊕, use docs#psum

[Riccardo Brasca]

You can use classical.some (half_prop x), but maybe it's not what you want.

[Riccardo Brasca]

BTW half_prop should be a lemma, not a def.

[Riccardo Brasca]

(The linter will flag this)

[Alex J. Best]

Using @Junyan Xu's recommendation

import tactic
def half' (x : ℕ) : Σ y, psum (2 * y = x)  (2 * y = x + 1) :=
begin
  induction x with x ih,
  { use 0, left, refl, },

  rcases ih with ⟨y, h | h⟩, -- can only eliminate into Prop
  { use y + 1,
    right,
    simp [mul_add, h], },
  { use y,
    left,
    exact h, },
end

[Aaron Bies]

Ah, it works with psum... why does it work with psum but not with sum?

[Junyan Xu]

psum (α : Sort u) (β : Sort v) can be applied to Prop because Prop is Sort 0.
sum (α : Type u) (β : Type v) can't be applied because Type u is Sort (u+1) so you can never get Sort 0.

[Aaron Bies]

Doesn't this mean one could always use psum instead of sum?

[Junyan Xu]

I think sum is better behaved with respect to universe level unification, because the resulting type is in Type (max u v), while psum has resulting type in Sort (max 1 u v). Is that the only reason? I don't know.

[Eric Wieser]

Yes, that is the reason

[Aaron Bies]

I need to read more about how universes work

[Aaron Bies]

Thank you