Coq Module Combined.

Inductive tm : Type :$=$

$|$ C : nat $->$ tm

$|$ P : tm $->$ tm $->$ tm

$|$ tru : tm

$|$ fls : tm

$|$ test : tm $->$ tm $->$ tm $->$ tm$.$

Inductive value : tm $->$ Prop :$=$

$|$ v$\_$const : forall n$,$ value $($C n$)$

$|$ v$\_$tru : value tru

$|$ v$\_$fls : value fls$.$

Reserved Notation $"$ t $\text{'}-->\text{'}$ t$\text{'}"($at level $40).$

Inductive step : tm $->$ tm $->$ Prop :$=$

$|$ ST$\_$PlusConstConst : forall v$1$ v$2,$

P $($C v$1)($C v$2)-->$ C $($v$1+$ v$2)$

$|$ ST$\_$Plus$1$ : forall t$1$ t$1\text{'}$ t$2,$

t$1-->$ t$1\text{'}->$

P t$1$ t$2-->$ P t$1\text{'}$ t$2$

$|$ ST$\_$Plus$2$ : forall v$1$ t$2$ t$2\text{'},$

value v$1->$

t$2-->$ t$2\text{'}->$

P v$1$ t$2-->$ P v$1$ t$2\text{'}$

$|$ ST$\_$IfTrue : forall t$1$ t$2,$

test tru t$1$ t$2-->$ t$1$

$|$ ST$\_$IfFalse : forall t$1$ t$2,$

test fls t$1$ t$2-->$ t$2$

$|$ ST$\_$If : forall t$1$ t$1\text{'}$ t$2$ t$3,$

t$1-->$ t$1\text{'}->$

test t$1$ t$2$ t$3-->$ test t$1\text{'}$ t$2$ t$3$

where $"$ t $\text{'}-->\text{'}$ t$\text{'}"$ :$=($step t t$\text{'}).$

$(**$ Earlier, we separately proved for both plus$-$ and if$-$expressions...

$-$ that the step relation was deterministic, and

$-$ a strong progress lemma, stating that every term is either a

value or can take a step.

Formally prove or disprove these two properties for the combined

language. $*)$

$(******$ Exercise: $3$ stars, standard $($combined$\_$step$\_$deterministic$)*)$

Theorem combined$\_$step$\_$deterministic: $($deterministic step$)\backslash /$ ~ $($deterministic step$).$

Proof.