✔ code stopped work · Coq users

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: Oct 13 2024 at 01:02 UTC