プログラミング言語の基礎概念
式の変形その1
Reserved Notation "e '==>' e'" (at level 50, left associativity).
Inductive ReduceNatExpR : Exp -> Exp -> Prop :=
| R_Plus : forall n1 n2 n3,
n1 plus n2 is n3 -> (ExpConst n1) +_ (ExpConst n2) ==> ExpConst n3
| R_Times : forall n1 n2 n3,
n1 times n2 is n3 -> (ExpConst n1) *_ (ExpConst n2) ==> ExpConst n3
| R_PlusL : forall e1 e1' e2,
e1 ==> e1' -> (e1 +_ e2) ==> (e1' +_ e2)
| R_PlusR : forall e1 e2 e2',
e2 ==> e2' -> (e1 +_ e2) ==> (e1 +_ e2')
| R_TimesL : forall e1 e1' e2,
e1 ==> e1' -> (e1 *_ e2) ==> (e1' *_ e2)
| R_TimesR : forall e1 e2 e2',
e2 ==> e2' -> (e1 *_ e2) ==> (e1 *_ e2')
where "e '==>' e'" := (ReduceNatExpR e e').その2
Reserved Notation "e '==>*' e'" (at level 50, left associativity).
Inductive ReduceNatExpRM : Exp -> Exp -> Prop :=
|MR_Zero : forall e, e ==>* e
|MR_One : forall e e', e ==> e' -> e ==>* e'
|MR_Multi : forall e e' e'',
e ==>* e' -> e' ==>* e'' -> e ==>* e''
where "e '==>*' e'" := (ReduceNatExpRM e e').
その3
Reserved Notation "e '==>d' e'" (at level 50, left associativity).
Inductive ReduceNatExpRD : Exp -> Exp -> Prop :=
| DR_Plus : forall n1 n2 n3,
n1 plus n2 is n3 -> (ExpConst n1) +_ (ExpConst n2) ==>d ExpConst n3
| DR_Times : forall n1 n2 n3,
n1 times n2 is n3 -> (ExpConst n1) *_ (ExpConst n2) ==>d ExpConst n3
| DR_PlusL : forall e1 e1' e2,
e1 ==> e1' -> (e1 +_ e2) ==>d (e1' +_ e2)
| DR_PlusR : forall n e2 e2',
e2 ==> e2' -> ((ExpConst n) +_ e2) ==>d ((ExpConst n) +_ e2')
| DR_TimesL : forall e1 e1' e2,
e1 ==> e1' -> (e1 *_ e2) ==>d (e1' *_ e2)
| DR_TimesR : forall n e2 e2',
e2 ==> e2' -> ((ExpConst n) *_ e2) ==>d ((ExpConst n) *_ e2')
where "e '==>d' e'" := (ReduceNatExpRD e e').
練習問題1-9
Example ex1_9_2 : ((ExpConst (S Z)) *_ (ExpConst (S Z)) +_ (ExpConst (S Z)) *_ (ExpConst (S Z))) ==>d (ExpConst (S Z) +_ ExpConst (S Z) *_ ExpConst (S Z)). Proof. apply DR_PlusL. apply R_Times. apply T_Succ with Z. apply T_Zero. apply P_Succ. apply P_Zero. Qed.
