(** Spring 2010 Coq project for the Formal Type Theory course

Replace the [Admitted] commands below with proper proof scripts. Add
definitions and auxiliary lemmas as you see fit. Return your solution to
lealanko@cs.helsinki.fi before the end of April 2010.

In your solution, you are free to copy and adapt definitions and proof
scripts from the course material. You can also use Coq's automation
facilities and this is in fact highly recommended.

If you are unable to solve a problem completely, do whatever you can:
isolate the minimal propositions that you are unable to solve formally
and assert them using [Admitted] or the [admit] tactic. In a comment,
provide a rationale (an informal proof) for why you think the
proposition should be true even if you are unable to prove it formally.

Please keep your proof scripts legible with judicious use of
indentation. It is of course also a good idea to comment your scripts.

*)

Require Import typed_por_lang.
Require Import tapl_ch3.

Notation "t1 -->* t2" := 
  (RSC eval t1 t2) (at level 80, no associativity) : type_scope.

(**

 The exercises concern a language with booleans, functions, and a new
boolean operator, a "parallel or" (or "por"), written [a || b]. The full
definition of the por operator can be found in the files por.ott and
typed_por_lang.v, but the most interesting evaluation rules are these:

t1 --> t1'
----------------------- :: Por1
t1 || t2  --> t1' || t2

t2 --> t2'
----------------------- :: Por2
t1 || t2  --> t1 || t2'

It should be immediately obvious that this language differs from those
in TAPL in the sense that it is non-deterministic: a term may be
evaluated to two distinct terms in a single step. Prove this.

*)

Lemma not_deterministic : ~(forall t t' t'', t --> t'  ->  t --> t''  ->  t' = t'').
(** Exercise **)
Admitted.

(**

 The progress property still holds, however. Prove this.

*)

Lemma progress : forall t T, |- t : T -> val t \/ exists t', t --> t'.
(** Exercise **)
Admitted.

(**

The por operator acts like a boolean or: an operation evaluates to
[true] if and only if at least one of the operands evaluates to [true].
Prove this.

*)

Lemma por_true_iff_operand_true : forall t1 t2,
  (t1 || t2)%tm -->* true%tm <-> (t1 -->* true%tm \/ t2 -->* true%tm).
(** Exercise **)
Admitted.

(**

(Side note: in our language the por operation is in fact redundant since
we could define por in terms of [if] and still have the above property
hold. However, this is only due to the fact that in the current language
every term is terminating. If we added the general recursion operator
[fix] into our language, this would no longer be true, and the
nondeterminism of the por operator would be crucial for ensuring that
[t1 || t2] evaluates to [true] if either [t1] or [t2] evaluates to true,
_even_ if the other operand diverges.)

Although our language is not deterministic, the nondeterminism is
well-behaved in the sense that no term can evaluate into two distinct
_values_: the nondeterminism only means that there are several
alternative intermediate steps in the evaluation, but the end result
will still be the same.

A related proposition is the following variant of the _diamond
property_: if a term [t1] can be evaluated into two distinct alternative
terms [t2] and [t3] in a single step, then there is some term [t4] into
which either of [t2] and [t3] can be evaluated in zero or more steps.
Prove this.



 *)

Lemma diamond : forall t1 t2 t3, 
  t2 <> t3 -> (t1 --> t2) -> (t1 --> t3) -> 
  exists t4, t2 -->* t4 /\ t3 -->* t4.
(** Exercise **)
Admitted.

(** **)