CODEWITHSUNDEEP
coq
Jimmy Stone
Jimmy Stone

Reputation: 121

How can I write a nat in the form of term?

All

I am trying to complete the last execrise in the StlcProp of Software Foundations Vol2. But I got stuck at defining step, in the rule ST_SuccNat.

Inductive step : tm -> tm -> Prop :=
  | ST_AppAbs : forall x T2 t1 v2,
      value v2 ->
      <{(\x:T2, t1) v2}> --> <{ [x:=v2]t1 }>
  | ST_App1 : forall t1 t1' t2,
      t1 --> t1' ->
      <{t1 t2}> --> <{t1' t2}>
  | ST_App2 : forall v1 t2 t2',
      value v1 ->
      t2 --> t2' ->
      <{v1 t2}> --> <{v1  t2'}>
  | ST_SuccNat: forall n:nat,
      <{succ n}> --> <{ S n }> (* <----- stuck here *)

Coq complains as below

In environment
step : tm -> tm -> Prop
n : nat
The term "S" has type "nat -> nat" while it is expected to have type "tm".

How can I tell Coq the S n in the form of "tm" ?

Thanks

Upvotes: 0

Views: 73

Answers (1)

Li-yao Xia
Li-yao Xia

Reputation: 33519

I think you can do

      <{succ n}> --> S n
(* which desugars to     succ (tm_const n) --> tm_const (S n) *)

The <{ }> brackets change the interpretation of application. Here you want the regular function application, so don't use the brackets.

Upvotes: 1

Related Questions