プログラミング言語の基礎概念

式の定義

Inductive Exp : Type :=
 | ExpConst : nat -> Exp
 | ExpPlus : Exp -> Exp -> Exp
 | ExpMult : Exp -> Exp -> Exp.
 
Notation "x '+_' y" := (ExpPlus x y) (at level 50): type_scope.
Notation "x '*_' y" := (ExpMult x y) (at level 40): type_scope.
Check (ExpConst (S Z)).
Check (ExpPlus (ExpConst (S Z)) (ExpConst Z)).
Check (ExpConst (S Z) +_ (ExpConst Z)).
Check (ExpConst (S Z) *_ (ExpConst Z)).
Check (ExpConst (S Z) *_ (ExpConst Z) +_ (ExpConst (S Z))).
Check (ExpConst (S Z) *_ ((ExpConst Z) +_ (ExpConst (S Z)))).

式の評価

Reserved Notation "e '||' n" (at level 50, left associativity).
 
Inductive EvalNatExpR : Exp -> nat -> Prop :=
 | E_Const : forall n, EvalNatExpR (ExpConst n) n
 | E_Plus : forall e1 e2 n1 n2 n3, 
    e1 || n1 ->
    e2 || n2 ->
    n1 plus n2 is n3 -> (e1 +_ e2) ||  n3
 | E_Times : forall e1 e2 n1 n2 n3, 
    e1 || n1 ->
    e2 || n2 ->
    n1 times n2 is n3 -> (e1 *_ e2) || n3
where "e '||' n" := (EvalNatExpR e n).

練習問題1-8

Example ex1_8_1 : 
  (ExpConst Z) +_  (ExpConst (S (S Z))) || S(S Z).
Proof.
apply E_Plus with (n1:=Z) (n2:=(S(S Z))).
constructor. constructor. constructor.
Show Proof.
(**
 ===>
(E_Plus (ExpConst Z) (ExpConst (S (S Z))) Z (S (S Z)) 
   (S (S Z)) (E_Const Z) (E_Const (S (S Z))) (P_Zero (S (S Z))))
*)
Qed.

ソフトウェアの基礎のImp_J.vの章の真似して書くことは書ける。

書いておいてなんだけど、未だに、この(数値|足し算|かけ算の)式と先日のnat plus/timesの区別がきっちり心のなかでついてない。

式上での足し算かけ算で、+*記号そのものがなんで使えないのかもよく分からない。

Notation "x '+' y" := (ExpPlus x y) (at level 50): type_scope.
(**
  ===>
Error: Notation _ + _ is already defined at level 50 with arguments
at level 50, at next level while it is now required to be at level 50
with arguments at next level, at next level.
*)