## Stream: general

### Topic: Working around the elimination restriction

#### Aaron Bies (Jun 10 2022 at 14:55):

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?

#### Riccardo Brasca (Jun 10 2022 at 15:01):

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

#### Riccardo Brasca (Jun 10 2022 at 15:02):

BTW half_prop should be a lemma, not a def.

#### Riccardo Brasca (Jun 10 2022 at 15:02):

(The linter will flag this)

#### Alex J. Best (Jun 10 2022 at 15:06):

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,
{ use y,
left,
exact h, },
end


#### Aaron Bies (Jun 10 2022 at 15:07):

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

#### Junyan Xu (Jun 10 2022 at 15:13):

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 (Jun 10 2022 at 15:16):

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

#### Junyan Xu (Jun 10 2022 at 15:24):

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 (Jun 10 2022 at 15:31):

Yes, that is the reason