Library combine_results

Require Import lang Vtac.

Notation "r1 # r2" := (res_combine r1 r2) (at level 60).

Lemma res_combine_values: forall r1 r2 e',
res_combine r1 r2 = Rval e' -> (exists v1, exists v2, r1 = (Rval v1) /\ r2 = (Rval v2) /\ e' = (Vpair v1 v2)).

Proof.
intros.
unfold res_combine in H.
induction r1; induction r2; try now inversion H.
exists v, v0.
split.
  reflexivity.
  split.
    reflexivity.
    injection H. clarify.
Qed.

Lemma res_combine_ptuple: forall r1 r2 r3 r4,
res_combine r1 r2 = (Rptuple r3 r4) -> (r1 = r3) /\ (r2 = r4).

Proof.
intros.
split;
induction r1; induction r2; try now inversion H.
Qed.

Lemma res_combine_bot : forall e r1 r2,
(Rbot e) = res_combine r1 r2 -> False.

Proof.
intros.
induction r1; induction r2; try now inversion H.
Qed.

Lemma res_combine_rletl : forall r x e r1 r2,
(Rletl r x e) = res_combine r1 r2 -> False.

Proof.
intros.
induction r1; induction r2; try now inversion H.
Qed.

Lemma res_combine_rletr : forall r r1 r2,
(Rletr r) = res_combine r1 r2 -> False.

Proof.
intros.
induction r1; induction r2; try now inversion H.
Qed.

Lemma res_combine_results: forall e r1 r2 r x,
((Rbot e) = res_combine r1 r2 \/
(Rletl r x e) = res_combine r1 r2 \/
(Rletr r) = res_combine r1 r2)
-> False.

Proof.
intros.
des; induction r1; induction r2; try now inversion H.
Qed.