The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

Inspired by this discussion, I've mocked up something that might be
able to serve as the beginnings of a combinatorics module for such a
class (and for Coq more generally).

Require Import Program.
Require Import List.
Generalizable All Variables.

Class Decision (P:Prop) : Set :=
| decide : {P} + {~P}.

Implicit Arguments decide [[Decision]].

Definition decideb (P:Prop) `{Decision P} : bool :=
if decide P then true else false.

Notation "'Yes'" := (left _ _).
Notation "'No'" := (right _ _).
Notation "'Reduce' x" := (if x then Yes else No) (at level 90).

Program Instance True_dec : Decision True := Yes.
Program Instance False_dec : Decision False := No.

Obligation Tactic := program_simpl; tauto.

Program Instance and_dec `{Decision P} `{Decision Q} :
  Decision (P /\ Q) :=
if decide P then
  Reduce (decide Q)
else
  No.

Program Instance or_dec `{Decision P} `{Decision Q} :
  Decision (P \/ Q) :=
if decide P then
  Yes
else
  Reduce (decide Q).

Program Instance not_dec `{Decision P} : Decision (~P) :=
if decide P then No else Yes.

Program Instance impl_dec `{Decision P} `{Decision Q} :
  Decision (P -> Q) :=
if decide P then
  Reduce (decide Q)
else
  Yes.

Obligation Tactic := program_simpl.

Program Instance Forall_dec `{forall x:A, Decision (P x)} :
  forall l:list A, Decision (Forall P l) :=
fix Forall_dec (l : list A) : Decision (Forall P l) :=
match l with
| nil => Yes
| x :: l' => if decide (P x) then
               Reduce (Forall_dec l')
             else
               No
end.
Solve Obligations using (program_simpl; red; inversion 1; auto).

Program Instance Exists_dec `{forall x:A, Decision (P x)} :
  forall l:list A, Decision (Exists P l) :=
fix Exists_dec (l : list A) : Decision (Exists P l) :=
match l with
| nil => No
| x :: l' => if decide (P x) then
               Yes
             else
               Reduce (Exists_dec l')
end.
Solve Obligations using (program_simpl; red; inversion 1; auto).

Class EqDec (A:Type) : Type :=
| eq_dec :> forall x y:A, Decision (x = y).

Instance bool_eq_dec : EqDec bool.
intros x y; red; decide equality.
Defined.


Class Enumeration (A:Type) : Type :=
| elements : list A.

Implicit Arguments elements [[Enumeration]].

Definition finite_card (A:Type) `{Enumeration A} : nat :=
  length (elements A).

(* I'm not sure whether it's better to require the enumeration be
   exhaustive and have no duplications, before allowing the application
   of this notation. *)
Notation "# A" := (finite_card A) (at level 0).

Instance sum_enum `{Enumeration A} `{Enumeration B} :
  Enumeration (A + B) :=
map inl (elements A) ++ map inr (elements B).

Fixpoint list_prod `(l1 : list A) `(l2 : list B) : list (A * B) :=
match l1 with
| nil => nil
| x :: l1' => map (pair x) l2 ++ list_prod l1' l2
end.

Instance prod_enum `{Enumeration A} `{Enumeration B} :
  Enumeration (A * B) :=
list_prod (elements A) (elements B).

Instance sig_enum `{Enumeration A} `{forall x:A, Decision (P x)} :
  Enumeration (sig P) :=
(fix filter (l : list A) : list (sig P) :=
  match l with
  | nil => nil
  | x :: l' => match decide (P x) with
               | left p => exist P x p :: filter l'
               | right _ => filter l'
               end
  end)
(elements A).

Instance bool_enum : Enumeration bool := [ false; true ].

Example size_bool : # bool = 2.
Proof. lazy. reflexivity. Qed.

Example size_sig_bool : # { b:bool | andb b false = b } = 1.
Proof. lazy. reflexivity. Qed.

Instance prod_dec `{forall (x:A) (y:B), Decision (P x y)} :
  forall p:A*B, Decision (let (x,y):=p in P x y) :=
fun p => match p with
| pair x y => decide (P x y)
end.

Example size_bool_le_rel :
  #({ (x,y):bool*bool | andb x y = x }) = 3.
Proof. lazy. reflexivity. Qed.


(* For some applications, such as sig when we're not assuming
   proof irrelevance, we might need to allow A to be a setoid and
   adjust this definition accordingly. *)
Class ExhaustiveEnumeration (A:Type) `{Enumeration A} : Prop :=
| exhaustivity : forall x:A, In x (elements A).

Instance bool_enum_exhaustive : ExhaustiveEnumeration bool.
Proof.
intro x; destruct x; simpl; auto.
Qed.

Program Instance forall_finite_dec `{ExhaustiveEnumeration A}
  `{forall x:A, Decision (P x)} : Decision (forall x:A, P x) :=
Reduce (decide (Forall P (elements A))).
Next Obligation.
rewrite Forall_forall in H2.
auto.
Defined.
Next Obligation.
rewrite Forall_forall in H2.
auto.
Defined.

Program Instance exists_finite_dec `{ExhaustiveEnumeration A}
  `{forall x:A, Decision (P x)} : Decision (exists x:A, P x) :=
Reduce (decide (Exists P (elements A))).
Next Obligation.
rewrite Exists_exists in H2.
destruct H2 as [x [? ?]]; exists x; trivial.
Defined.
Next Obligation.
red; destruct 1 as [x ?].
apply H2.
rewrite Exists_exists.
exists x; split; auto.
Defined.

Ltac proof_by_decision :=
match goal with
| |- ~ ?P =>
  let dec := (eval hnf in (decide P)) in
  match dec with
  | left _ => fail "statement being negated is true"
  | right ?np => exact np
  | _ => fail "could not decide statement"
  end
| |- ?P =>
  let dec := (eval hnf in (decide P)) in
  match dec with
  | left ?p => exact p
  | right _ => fail "statement is false"
  | _ => fail "could not decide statement"
  end
end.

Example demorgan_bool : forall x y:bool,
  negb (andb x y) = orb (negb x) (negb y).
Proof.
proof_by_decision.
Qed.
-- 
Daniel Schepler