Stream: Coq users

Topic: I don't know what to call it

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?

Johannes Hostert (May 14 2024 at 19:33):

Because `S n` is not definitionally equal to `n+1`

Pavel Shuhray (May 14 2024 at 19:37):

I want to use S n.

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.

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).
``````

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

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!

(deleted)

Pavel Shuhray (Jun 11 2024 at 02:32):

(deleted)

Last updated: Jun 13 2024 at 19:02 UTC