From 0e4874caf332975d80e24821268b8280b3b5e30f Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 17 Apr 2013 11:12:29 +0000 Subject: [PATCH] commit by user andrea --- weblib/While/semantics.ma | 77 ++++++++++++++++++++------------------- weblib/test.ma | 2 +- 2 files changed, 40 insertions(+), 39 deletions(-) diff --git a/weblib/While/semantics.ma b/weblib/While/semantics.ma index 5898be246..638b7ac91 100644 --- a/weblib/While/semantics.ma +++ b/weblib/While/semantics.ma @@ -3,51 +3,52 @@ include "While/syntax.ma". include "arithmetics/div_and_mod.ma". - (* state *) -img class="anchor" src="icons/tick.png" id="state"definition state ≝ a href="cic:/matita/While/syntax/Var.ind(1,0,0)"Var/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. +definition state ≝ Var → nat. -(* Semantics of Arithmetic expressions *) +definition eqvar ≝ λv1,v2. + match v1 with + [Id n => match v2 with [Id m => eqb n m]]. + +definition update : state → Var → nat → state ≝ λs,v,a,v1. + if eqvar v1 v then a else s v1. -pre class="smallmargin" style="display: inline;"img class="anchor" src="icons/tick.png" id="evalA"let rec evalA a s ≝ + +(* Semantics of Arithmetic expressions *) +pre class="smallmargin" style="display: inline;" +let rec evalA a s ≝ match a with [ Const n => n | Aid v => s v - | Add a b => evalA a sa title="natural plus" href="cic:/fakeuri.def(1)"+/aevalA b s - | Sub a b => evalA a sa title="natural minus" href="cic:/fakeuri.def(1)"-/aevalA b s - | Mul a b => evalA a sa title="natural times" href="cic:/fakeuri.def(1)"*/aevalA b s - | Div a b => a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"div/a (evalA a s) (evalA b s) - | Mod a b => a href="cic:/matita/arithmetics/div_and_mod/mod.def(3)"mod/a (evalA a s) (evalA b s) + | Add a b => evalA a s+evalA b s + | Sub a b => evalA a s-evalA b s + | Mul a b => evalA a s*evalA b s + | Div a b => div (evalA a s) (evalA b s) + | Mod a b => mod (evalA a s) (evalA b s) ] . -img class="anchor" src="icons/tick.png" id="exA1"example exA1: a href="cic:/matita/While/semantics/evalA.fix(0,0,4)"evalA/a ((a href="cic:/matita/While/syntax/Aexp.con(0,1,0)"Const/a a title="natural number" href="cic:/fakeuri.def(1)"2/a)a href="cic:/fakeuri.def(1)" title="Aexp plus"+/a(a href="cic:/matita/While/syntax/Aexp.con(0,1,0)"Const/a a title="natural number" href="cic:/fakeuri.def(1)"3/a)) (λx.a title="natural number" href="cic:/fakeuri.def(1)"0/a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="natural number" href="cic:/fakeuri.def(1)"5/a. -normalize ///pre. - -(* Boolean expressions *) -inductive Bexp : Type[0] ≝ - | BFalse : Bexp - | BTtrue : Bexp - | BNot : Bexp → Bexp - | BAnd : Bexp → Bexp → Bexp - | BOr : Bexp → Bexp → Bexp - | Eq : a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → Bexp - | LE : a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → Bexp -. - -interpretation "Bexp not" 'not x = (BNot x). -interpretation "Bexp and" 'and x y = (BAnd x y). -interpretation "Bexp or" 'or x y = (BOr x y). -interpretation "Bexp 'less or equal to'" 'leq x y = (LE x y). - -(* Commands *) -inductive Cmd : Type[0] ≝ - | Skip : Cmd - | Assign : Var → a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → Cmd - | Seq : Cmd → Cmd → Cmd - | If : a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"Bexp/a → Cmd → Cmd → Cmd - | While : a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"Bexp/a → Cmd → Cmd -. - - \ No newline at end of file +example exA1: evalA ((Const 2)+(Const 3)*(Aid (Id 2))) (λx.span style="text-decoration: underline;"1/span) = span style="text-decoration: underline;"5/span. +normalize // qed. + +let rec evalB b s ≝ + match b with + [ BFalse => false + | BTtrue => true + | BNot b => ¬(evalB b s) + | BAnd b1 b2 => evalB b1 s ∧ evalB b2 s + | BOr b1 b2 => evalB b1 s ∨ evalB b2 s pre class="smallmargin" style="display: inline;"/pre + | Eq a1 a2 => eqb (evalA a1 s) (evalA a2 s) + | LE a1 a2 => leb (evalA a1 s) (evalA a2 s) + ]. + +inductive Cmd_sem: Cmd → state → statepre class="smallmargin" style="display: inline;"→ Prop/pre≝ + | Skip_sem : \forall s. Cmd_sem Skip s s + | Assign_sem : \forall s,v,a. Cmd_sem (Assign v a) s (update s v (evalA a s)) + | Seq_sem : \forall c1,c2,s1,s2,s3. Cmd_sem c1 s1 s2 \to Cmd_sem c2 s2 s3 \to Cmd_sem (Seq c1 c2) s1 s3 + | If_sem_true : \forall b,ct,cf,s,st. evalB b s = true \to Cmd_sem ct s st \to Cmd_sem (If b ct cf) s st + | If_sem_false : \forall b,ct,cf,s,sf. evalB b s = false \to Cmd_sem cf s sf \to Cmd_sem (If b ct cf) s sf + | While_true : \forall b,c,s,s1,s2. evalB b s = true \to Cmd_sem c s s1 \to Cmd_sem (While b c) s1 s2 \to Cmd_sem (While b c) s s2 + | While_false : \forall b,c,s. evalB b s = false \to Cmd_sem (While b c) s s +./pre \ No newline at end of file diff --git a/weblib/test.ma b/weblib/test.ma index 63a4794a1..922d36cc2 100644 --- a/weblib/test.ma +++ b/weblib/test.ma @@ -55,4 +55,4 @@ * examples that the user is encouraged to try after chapter1.ma) * 3) follow the instructions in the script. * - *) + *) \ No newline at end of file -- 2.39.2