Pavel Shuhray (May 14 2024 at 19:21): 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).
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 defineInductive A : forall (n:nat), Set := | avar :> Var -> A 0 | alam : forall (n:nat), Var -> A n -> A (S n).
Thank you!
Pavel Shuhray (Jun 11 2024 at 02:29):(deleted)
Pavel Shuhray (Jun 11 2024 at 02:32):(deleted)
Last updated: Oct 13 2024 at 01:02 UTC