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?

Because `S n`

is not definitionally equal to `n+1`

I want to use S n.

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.

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

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

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)

(deleted)

Last updated: Jun 13 2024 at 19:02 UTC