Require Import ExtLib.Data.Map.FMapPositive.
Require Import ExtLib.Data.Eq.
Require Import ExtLib.Tactics.Injection.

Fixpoint pmap_lookup' (ts : pmap Type) (p : positive) : option Type :=
  match p with
    | xH => pmap_here ts
    | xI p => pmap_lookup' (pmap_right ts) p
    | xO p => pmap_lookup' (pmap_left ts) p
  end.

Record OneOf (ts : pmap Type) : Type := mkOneOf
(* Goal: @eq (option T) match pf in (eq _ x) return (option match x with | Some T => T | None => Empty_set end) with | eq_refl => @Some match pmap_lookup' ts p with | Some T => T | None => Empty_set end match @eq_sym (option Type) (pmap_lookup' ts p) (@Some Type T) pf in (eq _ x) return match x with | Some T => T | None => Empty_set end with | eq_refl => v end end (@Some T v) *)
{ index : positive
; value : match pmap_lookup' ts index with
            | None => Empty_set
            | Some T => T
          end
}.

(* Goal: @eq (option T) match pf in (eq _ x) return (option match x with | Some T => T | None => Empty_set end) with | eq_refl => @Some match pmap_lookup' ts p with | Some T => T | None => Empty_set end match @eq_sym (option Type) (pmap_lookup' ts p) (@Some Type T) pf in (eq _ x) return match x with | Some T => T | None => Empty_set end with | eq_refl => v end end (@Some T v) *)
Definition Into {ts} {T : Type} (n : positive) (pf : pmap_lookup' ts n = Some T)
: T -> OneOf ts :=
  match pf in _ = X return match X with
                           | Some T => T
                           | None => Empty_set
                           end -> OneOf ts
  with
  | eq_refl => @mkOneOf ts n
  end.

(* Goal: @eq (option T) match pf in (eq _ x) return (option match x with | Some T => T | None => Empty_set end) with | eq_refl => @Some match pmap_lookup' ts p with | Some T => T | None => Empty_set end match @eq_sym (option Type) (pmap_lookup' ts p) (@Some Type T) pf in (eq _ x) return match x with | Some T => T | None => Empty_set end with | eq_refl => v end end (@Some T v) *)
Fixpoint asNth' {ts : pmap Type} (p p' : positive)
: match pmap_lookup' ts p' with
    | None => Empty_set
    | Some T => T
  end -> option (match pmap_lookup' ts p with
                   | None => Empty_set
                   | Some T => T
                 end) :=
  match p as p , p' as p'
        return match pmap_lookup' ts p' with
                 | None => Empty_set
                 | Some T => T
               end -> option (match pmap_lookup' ts p with
                                | None => Empty_set
                                | Some T => T
                              end)
  with
    | xH , xH => Some
    | xI p , xI p' => asNth' p p'
    | xO p , xO p' => asNth' p p'
    | _ , _ => fun _ => None
  end.

(* Goal: @eq (option T) match pf in (eq _ x) return (option match x with | Some T => T | None => Empty_set end) with | eq_refl => @Some match pmap_lookup' ts p with | Some T => T | None => Empty_set end match @eq_sym (option Type) (pmap_lookup' ts p) (@Some Type T) pf in (eq _ x) return match x with | Some T => T | None => Empty_set end with | eq_refl => v end end (@Some T v) *)
Definition asNth {ts : pmap Type} (p : positive) (oe : OneOf ts)
: option (match pmap_lookup' ts p with
            | None => Empty_set
            | Some T => T
          end) :=
  @asNth' ts p oe.(index ts) oe.(value ts).

(* Goal: @eq (option T) match pf in (eq _ x) return (option match x with | Some T => T | None => Empty_set end) with | eq_refl => @Some match pmap_lookup' ts p with | Some T => T | None => Empty_set end match @eq_sym (option Type) (pmap_lookup' ts p) (@Some Type T) pf in (eq _ x) return match x with | Some T => T | None => Empty_set end with | eq_refl => v end end (@Some T v) *)
Definition OutOf {ts} {T : Type} (n : positive)
           (pf : pmap_lookup' ts n = Some T)
: OneOf ts -> option T :=
  match pf in _ = X return OneOf ts -> option match X with
                                              | None => Empty_set:Type
                                              | Some T => T
                                              end
  with
  | eq_refl => @asNth ts n
  end.

Lemma asNth'_get_lookup : forall p ts v, asNth' (ts:=ts) p p v = Some v.
Proof.
(* Goal: forall (p : positive) (ts : pmap Type) (v : match pmap_lookup' ts p with | Some T => T | None => Empty_set end), @eq (option match pmap_lookup' ts p with | Some T => T | None => Empty_set end) (@asNth' ts p p v) (@Some match pmap_lookup' ts p with | Some T => T | None => Empty_set end v) *)
  induction p; simpl; intros; auto.
Qed.

Theorem Outof_Into : forall ts T p pf v,
    @OutOf ts T p pf (@Into ts T p pf v) = Some v.
Proof using.
(* Goal: forall (ts : pmap Type) (T : Type) (p : positive) (pf : @eq (option Type) (pmap_lookup' ts p) (@Some Type T)) (v : T), @eq (option T) (@OutOf ts T p pf (@Into ts T p pf v)) (@Some T v) *)
  unfold OutOf, Into.
(* Goal: forall (o : option Type) (pf : @eq (option Type) o (@Some Type T)), @eq (option T) match pf in (eq _ x) return (option match x with | Some T => T | None => Empty_set end) with | eq_refl => @Some match o with | Some T => T | None => Empty_set end match @eq_sym (option Type) o (@Some Type T) pf in (eq _ x) return match x with | Some T => T | None => Empty_set end with | eq_refl => v end end (@Some T v) *)
  intros.
(* Goal: @eq (option T) (match pf in (eq _ X) return (forall _ : OneOf ts, option match X with | Some T => T | None => Empty_set end) with | eq_refl => @asNth ts p end (match pf in (eq _ X) return (forall _ : match X with | Some T => T | None => Empty_set end, OneOf ts) with | eq_refl => mkOneOf ts p end v)) (@Some T v) *)
  repeat rewrite (eq_Arr_eq pf).
(* Goal: @eq (option T) match pf in (eq _ x) return (option match x with | Some T => T | None => Empty_set end) with | eq_refl => @asNth ts p match @eq_sym (option Type) (pmap_lookup' ts p) (@Some Type T) pf with | eq_refl => match pf with | eq_refl => mkOneOf ts p match @eq_sym (option Type) (pmap_lookup' ts p) (@Some Type T) pf in (eq _ x) return match x with | Some T => T | None => Empty_set end with | eq_refl => v end end end end (@Some T v) *)
  repeat rewrite (eq_Const_eq pf).
(* Goal: @eq (option T) match pf in (eq _ x) return (option match x with | Some T => T | None => Empty_set end) with | eq_refl => @asNth ts p match @eq_sym (option Type) (pmap_lookup' ts p) (@Some Type T) pf with | eq_refl => mkOneOf ts p match @eq_sym (option Type) (pmap_lookup' ts p) (@Some Type T) pf in (eq _ x) return match x with | Some T => T | None => Empty_set end with | eq_refl => v end end end (@Some T v) *)
  repeat rewrite (eq_Const_eq (eq_sym pf)).
(* Goal: forall (ts : pmap Type) (p : positive) (oe : OneOf ts) (v : match pmap_lookup' ts p with | Some T => T | None => Empty_set end) (_ : @eq (option match pmap_lookup' ts p with | Some T => T | None => Empty_set end) (@asNth ts p oe) (@Some match pmap_lookup' ts p with | Some T => T | None => Empty_set end v)), @eq (OneOf ts) oe (mkOneOf ts p v) *)
  unfold asNth. simpl.
(* Goal: @eq (option T) match pf in (eq _ x) return (option match x with | Some T => T | None => Empty_set end) with | eq_refl => @asNth' ts p p match @eq_sym (option Type) (pmap_lookup' ts p) (@Some Type T) pf in (eq _ x) return match x with | Some T => T | None => Empty_set end with | eq_refl => v end end (@Some T v) *)
  rewrite asNth'_get_lookup.
(* Goal: @eq (option T) match pf in (eq _ x) return (option match x with | Some T => T | None => Empty_set end) with | eq_refl => @Some match pmap_lookup' ts p with | Some T => T | None => Empty_set end match @eq_sym (option Type) (pmap_lookup' ts p) (@Some Type T) pf in (eq _ x) return match x with | Some T => T | None => Empty_set end with | eq_refl => v end end (@Some T v) *)
  { generalize dependent (pmap_lookup' ts p).
(* Goal: forall (o : option Type) (pf : @eq (option Type) o (@Some Type T)), @eq (option T) match pf in (eq _ x) return (option match x with | Some T => T | None => Empty_set end) with | eq_refl => @Some match o with | Some T => T | None => Empty_set end match @eq_sym (option Type) o (@Some Type T) pf in (eq _ x) return match x with | Some T => T | None => Empty_set end with | eq_refl => v end end (@Some T v) *)
    intros. subst. reflexivity. }
Qed.

Theorem asNth_eq
: forall ts p oe v,
    @asNth ts p oe = Some v ->
(* Goal: @eq (option T) match pf in (eq _ x) return (option match x with | Some T => T | None => Empty_set end) with | eq_refl => @Some match pmap_lookup' ts p with | Some T => T | None => Empty_set end match @eq_sym (option Type) (pmap_lookup' ts p) (@Some Type T) pf in (eq _ x) return match x with | Some T => T | None => Empty_set end with | eq_refl => v end end (@Some T v) *)
    oe = {| index := p ; value := v |}.
Proof.
(* Goal: forall (ts : pmap Type) (p : positive) (oe : OneOf ts) (v : match pmap_lookup' ts p with | Some T => T | None => Empty_set end) (_ : @eq (option match pmap_lookup' ts p with | Some T => T | None => Empty_set end) (@asNth ts p oe) (@Some match pmap_lookup' ts p with | Some T => T | None => Empty_set end v)), @eq (OneOf ts) oe (mkOneOf ts p v) *)
  unfold asNth.
(* Goal: @eq (option Type) (@pmap_lookup Type p m1) (pmap_lookup' (@pmap_left Type (@Branch Type o m1 m2)) p) *)
  destruct oe; simpl.
(* Goal: forall (v : match pmap_lookup' ts p with | Some T => T | None => Empty_set end) (_ : @eq (option match pmap_lookup' ts p with | Some T => T | None => Empty_set end) (@asNth' ts p index0 value0) (@Some match pmap_lookup' ts p with | Some T => T | None => Empty_set end v)), @eq (OneOf ts) (mkOneOf ts index0 value0) (mkOneOf ts p v) *)
  revert value0. revert index0. revert ts.
  induction p; destruct index0; simpl; intros;
  solve [ congruence | eapply IHp in H; inversion H; clear H IHp; subst; auto ].
Qed.

Section elim.
(* Goal: @eq (option T) match pf in (eq _ x) return (option match x with | Some T => T | None => Empty_set end) with | eq_refl => @Some match pmap_lookup' ts p with | Some T => T | None => Empty_set end match @eq_sym (option Type) (pmap_lookup' ts p) (@Some Type T) pf in (eq _ x) return match x with | Some T => T | None => Empty_set end with | eq_refl => v end end (@Some T v) *)
  Context {T : Type}.
  Variable F : T -> Type.

  Fixpoint pmap_elim (R : Type) (ts : pmap T) : Type :=
    match ts with
      | Empty => R
      | Branch None l r => pmap_elim (pmap_elim R r) l
      | Branch (Some x) l r => F x -> pmap_elim (pmap_elim R r) l
    end.
End elim.

Fixpoint pmap_lookup'_Empty (p : positive) : pmap_lookup' Empty p = None :=
  match p with
    | xH => eq_refl
    | xO p => pmap_lookup'_Empty p
    | xI p => pmap_lookup'_Empty p
  end.

Definition OneOf_Empty (f : OneOf Empty) : False.
Proof.
(* Goal: False *)
  destruct f. rewrite pmap_lookup'_Empty in *.
(* Goal: False *)
  intuition congruence.
Defined.

Lemma pmap_lookup'_eq p m : pmap_lookup p m = pmap_lookup' m p.
Proof.
(* Goal: @eq (option Type) (@pmap_lookup Type p m) (pmap_lookup' m p) *)
  generalize dependent m. induction p; intuition.
(* Goal: @eq (option Type) (@pmap_lookup Type p m1) (pmap_lookup' (@pmap_left Type (@Branch Type o m1 m2)) p) *)
  simpl. destruct m. simpl. rewrite pmap_lookup'_Empty. reflexivity.
(* Goal: @eq (option Type) (@pmap_lookup Type (xO p) m) (pmap_lookup' m (xO p)) *)
  simpl in *. apply IHp.
(* Goal: @eq (option Type) (@pmap_lookup Type p m1) (pmap_lookup' (@pmap_left Type (@Branch Type o m1 m2)) p) *)
  simpl in *. destruct m. simpl. rewrite pmap_lookup'_Empty. reflexivity.
(* Goal: @eq (option Type) (@pmap_lookup Type p m1) (pmap_lookup' (@pmap_left Type (@Branch Type o m1 m2)) p) *)
  simpl. apply IHp.
Defined.

Global Instance Injective_OneOf m i1 i2 v1 v2
: Injective (@eq (OneOf m)
(* Goal: @eq (option T) match pf in (eq _ x) return (option match x with | Some T => T | None => Empty_set end) with | eq_refl => @Some match pmap_lookup' ts p with | Some T => T | None => Empty_set end match @eq_sym (option Type) (pmap_lookup' ts p) (@Some Type T) pf in (eq _ x) return match x with | Some T => T | None => Empty_set end with | eq_refl => v end end (@Some T v) *)
                 {| index := i1 ; value := v1 |}
(* Goal: @eq (option T) match pf in (eq _ x) return (option match x with | Some T => T | None => Empty_set end) with | eq_refl => @Some match pmap_lookup' ts p with | Some T => T | None => Empty_set end match @eq_sym (option Type) (pmap_lookup' ts p) (@Some Type T) pf in (eq _ x) return match x with | Some T => T | None => Empty_set end with | eq_refl => v end end (@Some T v) *)
                 {| index := i2 ; value := v2 |}) :=
(* Goal: @eq (option T) match pf in (eq _ x) return (option match x with | Some T => T | None => Empty_set end) with | eq_refl => @Some match pmap_lookup' ts p with | Some T => T | None => Empty_set end match @eq_sym (option Type) (pmap_lookup' ts p) (@Some Type T) pf in (eq _ x) return match x with | Some T => T | None => Empty_set end with | eq_refl => v end end (@Some T v) *)
{ result := exists pf : i2 = i1,
    v1 = match pf in _ = T return match pmap_lookup' m T with
                                  | None => Empty_set
                                  | Some T => T
                                  end with
         | eq_refl => v2
         end
; injection :=
    fun H =>
      match H in _ = h
            return exists pf : index _ h = i1 ,
          v1 = match
            pf in (_ = T)
            return
            match pmap_lookup' m T with
            | Some T0 => T0
            | None => Empty_set
            end
          with
          | eq_refl => value _ h
          end
      with
      | eq_refl => @ex_intro _ _ eq_refl eq_refl
      end
}.
