type definition

Inductive tm : Set :=
| tm_true : tm
| tm_false : tm
| tm_if : tm -> tm -> tm -> tm
| tm_zero : tm
| tm_succ : tm -> tm
| tm_pred : tm -> tm
| tm_iszero : tm -> tm


Inductive bvalue : tm -> Prop :=
| b_true : bvalue tm_true
| b_false : bvalue tm_false

Inductive nvalue : tm -> Prop :=
| n_zero : nvalue tm_zero
| n_succ : forall t,
	  nvalue t -> nvalue (tm_succ t)

Definition value (t : tm) : Prop := bvalue t \/ nvalue t

(* Defines the operational semantics *)
Inductive eval : tm -> tm -> Prop :=
| e_iftrue : forall t2 t3, eval (tm_if tm_true t2 t3) t2
| e_iffalse : forall t2 t3, eval (tm_if tm_false t2 t3) t3
| e_if : eval t1 t1' -> eval (tm_if t1 t2 t3) (tm_if t1' t2 t3)
| e_succ : forall t t', eval t t' -> eval (tm_succ t) (tm_succ t')
| e_predzero : eval (tm_pred tm_zero) tm_zero
| e_predsucc : forall t, nvalue t -> eval (tm_pred (tm_succ t)) t
| e_pred : forall t t', eval t t' -> eval (tm_pred t) (tm_pred t')
| e_iszerozero : eval (tm_iszero tm_zero) tm_true
| e_iszerosucc : forall t,
	nvalue t -> eval (tm_iszero (tm_succ t)) tm_false
| e_iszero : forall t t', eval t t' -> eval (tm_iszero t) (tm_iszero t')

Inductive eval_many : tm -> tm -> Prop :=
| m_refl: forall t, eval_many t t
| m_step : forall t t' u, eval t t' -> eval_many t' u -> eval_many t u

Definition normal_form (t : tm) : Prop := ~ exists t', eval t t'

Proof is composed of 'tactics'. A proof begins initially with one goal and no hypotheses.

Lemma e_succ_pred_succ : forall t, nvalue t -> eval (tm_succ  (tm_pred (tm_succ t))) (tm_succ t)

Let t be a tm.
intros Hn : converts an implication into a hypothesis Hn and a goal
Check e_succ : converts goal into a simpler form by applying e_succ rule.
apply e_succ
Check e_predsucc : converts goal into simpler form by applying e_predsucc rule
apply e_predsucc : results in 'nvalue t'
But that is one of our hypothesis Hn
apply Hn.
Qed.


Lemma m_succ_pred_succ : forall t, nvalue t -> eval_many (tm_succ (tm_pred (tm_succ t))) (tm_succ t)
intros Hn.
(We need to break eval_many into an 'eval' and another 'eval_many')
Check m_step.
apply m_step with (t' := tm_succ t).
(Notice that we required a t' to apply m_step which needs to be supplied by the user)
We get two goals as a result: eval (tm_succ (tm_pred (tm_succ t))) (tm_succ t)  _and_  eval_many (tm_succ t) (tm_succ t)
The second one can be proved by
Check m_refl.
apply m_refl.
Qed.
The first one can be proved by
Check e_succ_pred_succ.
apply e_succ_pred_succ.
Qed.

Lemma m_iftrue_step: forall t t1 t2 u, eval t tm_true -> eval_many t1 u -> eval_many (tm_if t t1 t2) u

intros H1 H2.
Check m_step.
apply m_step with (t' = tm_if tm_true t1 t2).
results in two goals
1. eval (tm_if t t1 t2) (tm_if tm_true t1 t2)
2. eval_many (tm_if tm_true t1 t2) u

For the first goal, apply e_if and H1.
For the second goal, apply m_step with t' = t1 to get two goals:
1. eval (tm_if tm_true t1 t2) t1
2. eval_many t1 u
The second one is proved by m_refl.
The first one can be simplified by applying e_iftrue, and proven.
The second one is one of our assumptions.


Reasoning by Cases:
Lemma e_iszero_nvalue : forall v, nvalue v -> eval (tm_iszero v) tm_true \/ eval (tm_iszero v) tm_false

intros v Hn.
destruct Hn. (produces two subgoals by breaking 'nvalue v' into 'nvalue tm_zero' and 'nvalue (tm_succ t)'). Each subgoal needs to be proven. Use 'left.' to prove first subgoal, 'right.' to prove second subgoal.


Functions and Conversion
-------------------------

Inductive bool_option : Set :=
| some_bool : bool -> bool_option
| no_bool : bool_option.

Inductive nat_option : Set :=
| some_nat : nat -> nat_option
| no_nat : nat_option.

Definition tm_to_bool (t: tm) : bool_option :=
	match t with
	| tm_true => some_bool true
	| tm_false => some_bool false
	| _ => no_bool.

Definition bool_to_tm (b: bool) : tm :=
	match b with
	| true => tm_true
	| false => tm_false
	end.

Definition is_bool (t: tm) : bool :=
	match tm_to_bool t with
	| some_bool _ -> true
	| no_bool -> false
	end.

(* {struct t} indicates thatthe function is guaranteed to
   terminate because it is defined by structural induction
	 on 't' *)
Fixpoint tm_to_nat (t: tm) {struct t} : nat_option :=
  match t with
	| tm_zero => some_nat 0
	| tm_succ t1 =>
	    match tm_to_nat t1 with
			| some_nat n => some_nat (S n)
	    | no_nat => no_nat
			end
	| _ => no_nat
end.

Fixpoint nat_to_tm (n : nat) {struct n} : tm :=
  match n with
	| 0 => tm_zero
	| S m => tm_succ (nat_to_tm m)
	end.

Lemma bool_tm_bool : forall b, tm_to_bool (bool_to_tm b) = some_bool b.
Proof. intros b. destruct b. simpl (bool_to_tm true). simpl. reflexivity.

(interp evaluates a tm expression 't' and returns a normal form)
Fixpoint interp (t : tm) {struct t} : tm :=
match t with
| tm_true => tm_true
| tm_false => tm_false
| tm_if t1 t2 t3 =>
  match interp t1 with
	| tm_true => interp t2
	| tm_false => interp t3
	| t4 => tm_if t4 t2 t3
	end
| tm_zero => tm_zero
| tm_succ t1 => tm_succ (interp t1)
| tm_pred t1 =>
  match interp t1 with
	| tm_zero => tm_zero
	| tm_succ t2 =>
	  match tm_to_nat t2 with
		| some_nat _ => t2
		| no_nat => tm_pred (tm_succ t2)
	  end
	| t2 => tm_pred t2
	end
| tm_iszero t1 =>
  match interp t1 with
	| tm_zero => tm_true
	| tm_succ t2 =>
	  match tm_to_nat t2 with
		| some_nat _ => tm_false
		| no_nat => tm_iszero (tm_succ t2)
	  end
	| t2 => tm_iszero t2
	end
end.

Lemma interp_reduces : forall t, eval_many t (interp t).