# Zulip Chat Archive

## 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 `Prop`

s 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 (Jun 10 2022 at 14:57):

Instead of ⊕, use docs#psum

#### 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,
simp [mul_add, h], },
{ 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

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

I need to read more about how universes work

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

Thank you

Last updated: Dec 20 2023 at 11:08 UTC