(** 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.

(****)
Hint Constructors term val eval type typing and or ex bound fvs RSC : por.

(** 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'').
(** **)Proof with eauto with por.
  intro det.
  discriminate (det ((true || true) || (true || true))%tm 
                    (true || (true || true))%tm 
                    ((true || true) || true)%tm)...
Qed.
(****)
Inductive bv : term -> Prop :=
| bv_true : bv true
| bv_false : bv false
.

Inductive fv : term -> Prop :=
| fv_abs x T t : fv (\x : T, t)
.

Definition tval T := match T with
                       | Bool%ty => bv
                       | (T1 -> T2)%ty => fv
                     end.

Hint Constructors bv fv.


Lemma canonical_forms : forall v T, val v -> |- v : T  -> tval T v.
Proof with eauto 10 with por.
  intros v T val_v v_T.
  inversion val_v; inversion v_T; subst; unfold tval; try discriminate...
Qed.

Hint Resolve canonical_forms.

(** The progress property still holds, however. Prove this.

*)

Lemma progress : forall t T, |- t : T -> val t \/ exists t', t --> t'.
(** **)Proof with eauto with por.
  intros t T t_T.
  remember {}%ctx as G.
  induction t_T; subst...
    destruct IHt_T1 as [val_t1 | [t' t1Et1]]...
    elim (canonical_forms t1 Bool)...
    inversion H.

    right.
    destruct IHt_T1 as [val_t1 | [t1' t1Et1']]...
    destruct IHt_T2 as [val_t2 | [t2' t2Et2']]...
    elim (canonical_forms t1 (T11 -> T12))...

    right.
    destruct IHt_T1 as [val_t1 | [t1' t1Et1']]...
    elim (canonical_forms t1 Bool)...
    destruct IHt_T2 as [val_t2 | [t2' t2Et2']]...
    elim (canonical_forms t2 Bool)...
Qed.
(**

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).
(** **)Proof with eauto with por.
  intros t1 t2.
  remember true%tm.
  split.
    remember (t1 || t2)%tm.
    intro t12Mt.
    induction t12Mt in t1, t2, Heqt, Heqt0 |- *; subst.
      inversion Heqt0.
      inversion H; subst...
        destruct IHt12Mt with t1' t2...
        destruct IHt12Mt with t1 t2'...

    intros [t1Mt | t2Mt].
      induction t1Mt; subst...
      induction t2Mt; subst...
Qed.
(**

(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.

**)
Definition normal_form t := ~(exists t', t --> t').

Lemma val_is_normal : forall t, val t -> normal_form t.
Proof.
  intros t val_t [t' tEt'].
  inversion val_t; subst; inversion tEt'.
Qed.
  
Lemma if_mcongr : forall t1 t1' t2 t3, t1 -->* t1' ->
  (if t1 then t2 else t3)%tm -->* (if t1' then t2 else t3)%tm.
Proof with eauto with por.
  intros t1 t1' t2 t3 t1Mt1'.
  induction t1Mt1'...
Qed.

Lemma if_app1 : forall t1 t1' t2, t1 -->* t1' ->
  (t1 $ t2)%tm -->* (t1' $ t2)%tm.
Proof with eauto with por.
  intros t1 t1' t2 t1Mt1'.
  induction t1Mt1'...
Qed.

Lemma if_app2 : forall v1 t2 t2', val v1 -> t2 -->* t2' ->
  (v1 $ t2)%tm -->* (v1 $ t2')%tm.
Proof with eauto with por.
  intros v1 t2 t2' val_v1 t2Mt2'.
  induction t2Mt2'...
Qed.

Lemma if_por1 : forall t1 t1' t2, t1 -->* t1' -> (t1 || t2)%tm -->* (t1' || t2)%tm.
Proof with eauto with por.
  intros t1 t1' t2 t1Mt1'.
  induction t1Mt1'...
Qed.

Lemma if_por2 : forall t1 t2 t2', t2 -->* t2' -> (t1 || t2)%tm -->* (t1 || t2')%tm.
Proof with eauto with por.
  intros t1 t2 t2' t2Mt2'.
  induction t2Mt2'...
Qed.


Hint Resolve if_mcongr if_app1 if_app2 if_por1 if_por2.

(** *)

Lemma diamond : forall t1 t2 t3, 
  t2 <> t3 -> (t1 --> t2) -> (t1 --> t3) -> 
  exists t4, t2 -->* t4 /\ t3 -->* t4.
(** **)Proof with eauto 10 with por.
  intros t1 t2 t3 t2Nt3 t1Et2 t1Et3.
  induction t1 in t2, t3, t2Nt3, t1Et2, t1Et3 |- *; try solve [inversion t1Et2].

  inversion t1Et2; subst;
    inversion t1Et3; subst; try solve [inversion H3]...
      destruct IHt1_1 with t1' t1'0 as [t1'' [HA HB]]...
      intro.
      subst...
      
  inversion t1Et2; subst; inversion t1Et3; subst...
      destruct IHt1_1 with t1' t1'0 as [t1'' [HA HB]]...
      intro.
      subst...

      inversion H1; subst; inversion H2.

      inversion H2.

      inversion H1; subst; inversion H4.

      destruct IHt1_2 with t2' t2'0 as [t2'' [HA HB]]...
      intro.
      subst...

      inversion H4; subst; inversion H3.

      inversion H3.

      inversion H2; subst; inversion H4.

  inversion t1Et2; subst; inversion t1Et3; subst; try solve [inversion H2]...
      destruct IHt1_1 with t1' t1'0 as [t1'' [HA HB]]...
      intro.
      subst...
      
      destruct IHt1_2 with t2' t2'0 as [t2'' [HA HB]]...
      intro.
      subst...
Qed.
(** **)