notation-printing.v

From Coq Require Export Utf8.
From Coq.ssr Require Export ssreflect.
Set Default Proof Using "Type".

(** Telescopes *)
Inductive tele : Type :=
| TeleO : tele
| TeleS {X} (binder : X → tele) : tele.

Arguments TeleS {_} _.

Implicit Type (TT: tele).

(** The telescope version of Coq's [forall] *)
Fixpoint tforall (TT : tele) (T : Type) : Type :=
  match TT with
  | TeleO => T
  | TeleS b => forall x, tforall (b x) T
  end.

Notation "TT -t> A" :=
  (tforall TT A) (at level 99, A at level 200, right associativity).

(** An eliminator for elements of [tforall].
    We use a [fix] because, for some reason, that makes stuff print nicer
    in the proofs in bi/lib/telescopes.v *)
Definition tforall_fold {X Y} {TT : tele} (step : ∀ {A : Type}, (A → Y) → Y) (base : X → Y)
  : (TT -t> X) → Y :=
  (fix rec {TT} : (TT -t> X) → Y :=
     match TT as TT return (TT -t> X) → Y with
     | TeleO => λ x : X, base x
     | TeleS b => λ f, step (λ x, rec (f x))
     end) TT.
Arguments tforall_fold {_ _ !_} _ _ _ /.

(** A sigma-like type for an "element" of a telescope, i.e. the data it
  takes to get a [T] from a [tforall TT T]. *)
Inductive tele_arg : tele → Type :=
| TargO : tele_arg (TeleO)
(* the [x] is the only relevant data here *)
| TargS {X} {binder} (x : X) : tele_arg (binder x) → tele_arg (TeleS binder).

Coercion tele_arg : tele >-> Sortclass.

Definition tele_app {T} {TT : tele} (f : TT -t> T) (a : TT) : T :=
  (fix rec {TT} (a : TT) : (TT -t> T) → T :=
     match a in tele_arg TT return (TT -t> T) → T with
     | TargO => λ t : T, t
     | TargS x a => λ f, rec a (f x)
     end) TT a f.
Arguments tele_app {_ !_} _ !_ /.

Notation "f $$ a" :=
  (tele_app f a) (at level 65, right associativity).

(** Inversion lemma for [tele_arg] *)
Lemma tele_arg_inv {TT : tele} (a : TT) :
  match TT as TT return tele_arg TT → Prop with
  | TeleO => λ a, a = TargO
  | TeleS f => λ a, exists x a', a = TargS x a'
  end a.
Proof. induction a => //. eauto. Qed.
Lemma tele_arg_O_inv (a : tele_arg TeleO) : a = TargO.
Proof. by have:= tele_arg_inv a. Qed.
Lemma tele_arg_S_inv {X} {f : X → tele} (a : tele_arg (TeleS f)) :
  exists x a', a = TargS x a'.
Proof. by have:= tele_arg_inv a. Qed.

(** Map below a tforall *)
Fixpoint tforall_map {T U} {TT : tele} : (T → U) → (TT -t> T) → TT -t> U :=
  match TT as TT return (T → U) → (TT -t> T) → TT -t> U with
  | TeleO => λ F : T → U, F
  | @TeleS X b => λ (F : T → U) (f : TeleS b -t> T) (x : X),
                  tforall_map F (f x)
  end.
Arguments tforall_map {_ _ !_} _ _ /.

(** Map below a tforall *)
Fixpoint tforall_bind' {U} {TT : tele} : ((forall T, (TT -t> T) → T) → U) → TT -t> U :=
  match TT as TT return ((forall T, (TT -t> T) → T) → U) → TT -t> U with
  | TeleO => λ F, F (λ _ x, x)
  | @TeleS X b => λ F (x : X), tforall_bind' (λ tapp, F (λ _ th, tapp _ (th x)))
  end.
Arguments tforall_bind' {_ !_} _ /.

Fixpoint tforall_bind {U} {TT : tele} : (TT → U) → TT -t> U :=
  match TT as TT return (TT → U) → TT -t> U with
  | TeleO => λ F, F TargO
  | @TeleS X b => λ (F : TeleS b → U) (x : X), (* b x -t> U *)
                  tforall_bind (λ a, F (TargS x a))
  end.
Arguments tforall_bind {_ !_} _ /.

(** A function that looks funny. *)
Definition tele_arg_id (TT : tele) : TT -t> TT := tforall_bind (@id _).

(** Playground for THE BUG *)
Section bug.
Context (atomic_update :
           ∀ PROP : Type, ∀ A B : Type, (A → PROP) → (A → B → PROP) → PROP).
Context (PROP val loc : Type) (mapsto : loc → val → PROP).

Notation "'AU' ∀ x1 .. xn , α | ∃ y1 .. yn , β" :=
  (atomic_update _
                 (tele_arg (TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )))
                 (tele_arg (TeleS (fun y1 => .. (TeleS (fun yn => TeleO)) .. )))
                 (tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. ))
                           (fun x1 => .. (fun xn => α) ..))
                 (tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. ))
                           (fun x1 => .. (fun xn =>
                                            tele_app
                                              (TT:=TeleS (fun y1 => .. (TeleS (fun yn => TeleO)) .. ))
                                              (fun y1 => .. (fun yn => β) .. )) ..))
  )
  (at level 20, α at level 200, x1 binder, xn binder, y1 binder, yn binder).

Notation "'AU' ∀ x1 .. xn , α | β" :=
  (atomic_update _
                 (tele_arg (TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )))
                 (tele_arg TeleO)
                 (tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. ))
                           (fun x1 => .. (fun xn => α) ..))
                 (tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. ))
                           (fun x1 => .. (fun xn _ => β) ..))
  )
  (at level 20, α at level 200, x1 binder, xn binder).

Definition test1 := AU ∀ v l, mapsto v l | ∃ l', mapsto v l'.
Print test1.

Definition test2 := AU ∀ v l, mapsto v l | mapsto v l.
Print test2.