Discriminator and Projector for Some in option type

some.v

From Coq Require Import ssreflect.
From Coq Require Import StrictProp.
From Coq Require Import List.

(* Access to nth element of a list,
   stdpp's notation for simpler test writing *)
Notation "l !! n" := (nth_error l n) (at level 20).


(** Discriminator for Some *)
(* with value in SProp for irrelevance *)

Definition isSome [A : Type] (x : option A) : SProp :=
  match x with None => sEmpty | Some _ => sUnit end.

(** Partial Projector for Some *)
(*  with explicit proof *)

Definition Somepf [A : Type] (x : option A) : isSome x -> A :=
  match x with None => sEmpty_rect _ | Some x => fun _ => x end.

(* Notation for specifying only the term to be projected *)
(* tweak discharge_is_some to change inference of proofs *)
Ltac discharge_is_some := assumption.
Notation "'Somev' x" := (Somepf x ltac:(discharge_is_some)) (at level 10, only parsing).
Notation "'Somev' x" := (Somepf x _) (at level 10, only printing).


(** Tests *)

Check (fun A (x : option A) (p : isSome x) => Somev x).

Ltac discharge_is_some ::= intuition.
Check (fun A (f : A -> option A) (p : forall x, isSome (f x)) (a  : A) => Somev (f a)).


(** Building predicates using discriminators/projectors for Some *)

(* Notation for a dependent conjunction with first component in SProp *)
Definition depand (P : SProp) (Q : P -> Prop) : Prop := (Box P) /\ (forall p, Q p).

Notation "P ⊗ Q" := (depand P (fun _ => Q)) (at level 70, Q at level 200).


Definition is_zero (l : list nat) (n : nat) : Prop :=
  isSome (l !! n) ⊗ Somev (l !! n) = 0.




(** Lemmas to introduce Some from the discriminator *)

Lemma isSomeP [A : Type] (P : option A -> Prop) :
  (forall x, isSome x -> P x) <-> forall x (p : isSome x), P (Some (Somev x)).
Proof.
  split; move=> h [] // a p ; exact (h (Some a) p).
Qed.

Lemma isSomeP2 [A : Type] (P : option A -> Prop) (Q : A -> Prop) :
  (forall x, isSome x -> P x) ->
  (forall a, P (Some a) -> Q a) ->
  forall x (p : isSome x), Q (Somev x).
Proof.
  move=> /isSomeP h1 h2 x p; apply: h2; by apply: h1.
Qed.