## Stream: Coq users

### Topic: ✔ code stopped work

#### Andrey Klaus (Sep 02 2021 at 08:36):

Hello.
About half year ago code below worked

``````Inductive even : nat -> Type :=
| EZ : even 0
| ES : forall n, odd n -> even (S n)
with odd : nat -> Type :=
| OS : forall n, even n -> odd (S n).

Fixpoint even_sum n1 n2 (e1 : even n1) : even n2 -> even (n1 + n2) :=
match e1 with
| EZ => fun e2 => e2
| ES _ o1 => fun e2 => ES (odd_sum o1 e2)
end
with odd_sum n1 n2 (o : odd n1) : even n2 -> odd (n1 + n2) :=
match o with
| OS _ e => fun e2 => OS (even_sum e e2)
end.
``````

Now it gives me next error:

``````Error:
In environment
even_sum : forall n1 n2 : nat, even n1 -> even n2 -> even (n1 + n2)
odd_sum : forall n1 n2 : nat, odd n1 -> even n2 -> odd (n1 + n2)
n1 : nat
n2 : nat
e1 : even n1
e2 : even n2
The term "e2" has type "even n2" while it is expected to have type "even (?n@{n0:=0} + n2)".
``````

As I see, it is not able to compute that 0 + n2 is n2 anymore (but i'm not sure why it says about n0 instead of n...).
How to fix?

#### Olivier Laurent (Sep 02 2021 at 08:57):

Maybe there is something about implicit arguments, but at least (with explicit arguments) the following seems to work:

``````Fixpoint even_sum n1 n2 (e1 : even n1) : even n2 -> even (n1 + n2) :=
match e1 with
| EZ => fun e2 => e2
| ES _ o1 => fun e2 => ES _ (odd_sum _ _ o1 e2)
end
with odd_sum n1 n2 (o : odd n1) : even n2 -> odd (n1 + n2) :=
match o with
| OS _ e => fun e2 => OS _ (even_sum _ _ e e2)
end.
``````

#### Olivier Laurent (Sep 02 2021 at 08:59):

and with implicit arguments:

``````Set Implicit Arguments.

Inductive even : nat -> Type :=
| EZ : even 0
| ES : forall n, odd n -> even (S n)
with odd : nat -> Type :=
| OS : forall n, even n -> odd (S n).

Fixpoint even_sum n1 n2 (e1 : even n1) : even n2 -> even (n1 + n2) :=
match e1 with
| EZ => fun e2 => e2
| ES o1 => fun e2 => ES (odd_sum o1 e2)
end
with odd_sum n1 n2 (o : odd n1) : even n2 -> odd (n1 + n2) :=
match o with
| OS e => fun e2 => OS (even_sum e e2)
end.
``````

#### Andrey Klaus (Sep 02 2021 at 09:00):

Thank you. I think I forgot about Set Implicit Arguments or something like.

#### Notification Bot (Sep 02 2021 at 10:02):

Andrey Klaus has marked this topic as resolved.

Last updated: May 18 2024 at 10:02 UTC