Library boollogic
Require Import ssreflect.
Require Import ssrbool.
Require Import ssrnat.
Require Import ssrfun.
Require Import eqtype.
Require Import seq.
Require Import fintype.
Require Import finfun.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Universal quantification on finite types
Definition iforall (d : finType) (f : d->bool):=
(fgraph_of_fun f) == (fgraph_of_fun (fun _ => true)).
Definition iforall2 (d1 d2 : finType) (f : d1->d2->bool):=
iforall (fun xy => f xy.1 xy.2).
Definition iforall3 (d1 d2 d3 : finType) (f : d1->d2->d3->bool):=
iforall (fun xyz => f xyz.1.1 xyz.1.2 xyz.2).
Lemma iforallPx: forall (d:finType) (p:d->bool),
reflect (forall x, p x) (iforall p).
Proof.
move=>d p.
case H: (iforall p).
by apply: Reflect_true=>x; rewrite /iforall in H;
move: (fgraph_of_fun_inj (eqP H) x).
apply: Reflect_false=>K.
have L: (iforall p) by apply/eqP; apply: fgraph_of_fun_congr=>x; rewrite K.
by rewrite L in H.
Qed.
Lemma iforallPnx: forall (d:finType) (p:d->bool),
reflect (exists x, negb (p x)) (negb (iforall p)).
Proof.
move=>d p.
case H: (negb (iforall p)).
apply: Reflect_true.
case: (pickP (fun x=> negb (p x)))=>[x xm|e].
by exists x.
have K: iforall p.
apply/(iforallPx _)=>x.
by move: (negbEF (e x)).
by rewrite K in H.
by apply: Reflect_false; elim=>x; rewrite (iforallPx _ (negbEF H) x).
Qed.
Lemma iforall2Px: forall (d1 d2:finType) (p:d1->d2->bool),
reflect (forall x y, p x y) (iforall2 p).
Proof.
move=>d1 d2 p.
case H: (iforall2 p).
by apply: Reflect_true=>x y; move: (iforallPx _ H (x, y)).
apply: Reflect_false=>K.
have L: (iforall2 p) by apply/eqP; apply: fgraph_of_fun_congr=>x; rewrite K.
by rewrite L in H.
Qed.
Lemma iforall3Px: forall (d1 d2 d3:finType) (p:d1->d2->d3->bool),
reflect (forall x y z, p x y z) (iforall3 p).
Proof.
move=>d1 d2 d3 p.
case H: (iforall3 p).
by apply: Reflect_true=>x y z; move: (iforallPx _ H ((x, y), z)).
apply: Reflect_false=>K.
have L: (iforall3 p) by apply/eqP; apply: fgraph_of_fun_congr=>x; rewrite K.
by rewrite L in H.
Qed.
Notation iforallP := (iforallPx _).
Notation iforallPn := (iforallPnx _).
Notation iforall2P := (iforall2Px _).
Notation iforall3P := (iforall3Px _).