Stream: Coq users

Topic: I don't know what to call it


view this post on Zulip Pavel Shuhray (May 14 2024 at 19:21):

Hi
Var is the set of variables. Lam is the type of lambda-terms without applications. A (n) is the type of lambda-terms with n lambdas. rank(M) is the number of lambdas in M. There are problems with the function "bar".

Parameter Var : Set.

Inductive Lam : Set :=
| var :> Var -> Lam
| lam :  Var -> Lam -> Lam.

Inductive A : forall (n:nat), Set :=
| avar  :> Var -> A 0
| alam  : forall (n:nat), Var -> A n -> A (n+1).

Fixpoint rank (M:Lam) : nat :=
match M with
| var x => 0
| lam x M => S (rank M)
end.

Fixpoint bar (M:Lam) : A (rank M) :=
match M  with
| var x => x
| lam x M => alam (rank M) x (bar M)
end.

If I write

Fixpoint rank (M:Lam) : nat :=
match M with
| var x => 0
| lam x M =>   (rank M)  + 1
end.

problems disappear! Why?

view this post on Zulip Johannes Hostert (May 14 2024 at 19:33):

Because S n is not definitionally equal to n+1

view this post on Zulip Pavel Shuhray (May 14 2024 at 19:37):

I want to use S n.

view this post on Zulip Thomas Lamiaux (May 14 2024 at 19:50):

I am a bit surprised by the error message, but as said by Johannes the reason is that S n = 1 + n is not equal by definition to n + 1.
With the first definition, in the lam branch you are supposed to build a term of type A (1+n), but by definition alam builds a term of type A(n+1) which are not definitionally the same as 1 + n and n+1 are not the same by definition.

view this post on Zulip Thomas Lamiaux (May 14 2024 at 19:50):

If you want to use S n := 1 + n, you must define

Inductive A : forall (n:nat), Set :=
| avar  :> Var -> A 0
| alam  : forall (n:nat), Var -> A n -> A (S n).

view this post on Zulip Gaëtan Gilbert (May 14 2024 at 20:07):

the not nice error message is similar to the one in https://github.com/coq/coq/issues/11087, see discussion there

view this post on Zulip Pavel Shuhray (May 14 2024 at 20:10):

Thomas Lamiaux said:

If you want to use S n := 1 + n, you must define

Inductive A : forall (n:nat), Set :=
| avar  :> Var -> A 0
| alam  : forall (n:nat), Var -> A n -> A (S n).

Thank you!

view this post on Zulip Pavel Shuhray (Jun 11 2024 at 02:29):

(deleted)

view this post on Zulip Pavel Shuhray (Jun 11 2024 at 02:32):

(deleted)


Last updated: Jun 13 2024 at 19:02 UTC