Mapping existential statements.

mapex.coq

(** A "function" of the form [forall x, exists y, R x y] can be mapped
over a list [l], and produces [exists l', Forall2 R l l'], where
[Forall2 R l l'] means that [l] and [l'] have the same length and
elements at corresponding positions are related by [R].
We basically use the fact that the propositional truncation (written
[[A]] in this file) is a monad, and lists are traversable
(see http://hackage.haskell.org/package/base-4.7.0.0/docs/Data-Traversable.html )
*)
 
Require Import Coq.Lists.List.
 
Inductive Inhabited (A:Type) : Prop :=
| prf (a:A)
.
Arguments prf {A} a.
 
Notation "[ A ]" := (Inhabited A).
Notation "⟨ a ⟩" := (prf a).
 
(* [l] and [q] have the same length and corresponding elements are related *)
Fixpoint Forall2 {A B} (l:list A) (q:list B) (R:A->B->Prop) : Prop :=
match l,q with
| nil,nil => True
| a::r, b::s => R a b /\ (Forall2 r s R)
| _,_ => False
end
.
 
(* [exists x, P x] is the same as [[{x:A|P x}]]. I'll use only the
latter in the rest of the file. *)
Remark ex_inh : forall A (P:A->Prop), (exists x:A, P x) <-> [{x:A|P x}].
Proof.
intros *. split.
+ intros [x h].
constructor.
eexists; eauto.
+ intros [[x h]].
eexists; eauto.
Qed.
 
(** A variant of [list] relative to another list:
[list P [x₁;…;xn]] is a list [y₁;…;yn] where
[y₁:P x₁], …, [yn:P xn]. *)
Fixpoint list_ {A} (P:A->Type) (l:list A) : Type :=
match l with
| nil => unit
| a::r => (P a * list_ P r)%type
end
.
 
(** Equivalent of [List.map] for [list_]. *)
Fixpoint map_dep {A} {P:A->Type} (f:forall x:A, P x) (l:list A) : list_ P l :=
match l with
| nil => tt
| a::r => (f a, map_dep f r)
end
.
 
(** Pairs are traversable (special case of truncation). *)
Definition pair_inh {A B} (x:[A]) (y:[B]) : [A*B] :=
match x,y with (* uses that both [A*B] and [B]->[A*B] are propositions*)
| ⟨x'⟩,⟨y'⟩ => ⟨(x',y')⟩
end
.
 
(** The type [list_ P l] is traversable (special case of truncation. *)
Fixpoint traverse_inh {A} {P:A->Type} {l:list A} : (list_ (fun x => [P x]) l) -> [list_ P l] :=
match l with
| nil => fun q => ⟨tt⟩ (* = ⟨q⟩ *)
| a::r => fun q => pair_inh (fst q) (traverse_inh (snd q))
end
.
 
(** The first projection of the elements of a [list_] of sigmas is a proper list. *)
Fixpoint map_proj1 {A B} {R:A->B->Prop} {l:list A} : (list_ (fun x => {y:B|R x y}) l) -> list B :=
match l with
| nil => fun _ => nil
| a::r => fun q => proj1_sig (fst q) :: map_proj1 (snd q)
end
.
 
(** [map_proj1] preserves the relation with the list [l]. *)
Lemma map_proj1_related A B (R:A->B->Prop) (l:list A) (q:list_ (fun x => {y:B|R x y}) l) : Forall2 l (map_proj1 q) R.
Proof.
induction l as [ | a r h ].
+ easy.
+ simpl in q. destruct q as [ [ hd hhd ] tl ]. simpl.
now split.
Qed.
 
(** When proving a proposition, I can assume I have a list obtained by
"mapping" a proposition of the form ∀∃. *)
Theorem map_existential A B (R:A->B->Prop) (l:list A) (P:Prop) :
(forall q:list B, Forall2 l q R -> P) -> (forall x, [{y:B|R x y}]) -> P.
Proof.
intros h f.
generalize (map_dep f l); intros q.
apply traverse_inh in q. destruct q as [q].
apply h with (map_proj1 q).
apply map_proj1_related.
Qed.