1
$\begingroup$

Coq beginner here! My question is how to formalize reasoning of the kind "...consider the following function, it has some property, therefore..." in Coq. The challenge is to prove the existence of a function with that property. I think that I could use something like the epsilon operator, but I'd like to be sure that I'm assuming nothing stronger than I need. I'm happy to assume classical logic if that helps.

As an example, here's a simplified informal version of what I'm trying to prove:

Let $U$ be a (non-empty) set (could be finite or infinite). Let $A,B \subseteq U$ and $C \subseteq \mathbb{N}^U$ (i.e. $C$ is a set of functions from $U$ to $\mathbb{N}$). We have the following two principles:

Equality If $f \in \mathbb{N}^U$ and $f(i)=0$ for all $i \in A$, then $f \not\in C$.

Dominance If $f \in \mathbb{N}^U$ and $f(i) \geq 0$ for all $i \in B$ and $f(i) > 0$ for some $i \in B$, then $f \in C$.

Then:

Theorem: $B \subseteq A$ follows from Equality and Dominance.

Proof: Consider the function $$f(i)= \begin{cases} 0 & \text{if } i \in A \\ 1 & \text{otherwise}\end{cases}$$ By Equality, $f \not\in C$. Clearly $f(i) \geq 0$ for all $i \in B$. Moreover, if $B \not\subseteq A$, then there's some $i \in B$ such that $f(i)>0$, so that by Dominance $f \in C$. Thus, $B \subseteq A$.

Here's what I have so far in Coq:

Parameter U : Set.
Parameter A B : U -> Prop.
Parameter C : (U -> nat) -> Prop.

Definition Equality : Prop := forall (f : U -> nat), (forall (i : U), A i -> f i = 0) -> ~ C f.

Definition Dominance : Prop := forall (f : U -> nat),
 (forall (i : U), B i -> (f i) >= 0)/\ (exists (i : U), B i /\ (f i) > 0) -> C f.

Theorem B_subset_A : Equality /\ Dominance -> forall (i : U), B i -> A i.

Because Coq doesn't allow one to define functions in terms of Props, I can't just define the $f$ in the informal proof out of nothing. So what do I need to prove B_subset_A in a way that's analogous to the informal proof?

$\endgroup$
1
  • 1
    $\begingroup$ Do you mean you want to case split on whether $i \in A$? You need the excluded middle, not the epsilon operator (although that incidentally also gives you excluded middle). Alternatively, you can also assume $A$ is decidable. $\endgroup$
    – Trebor
    Aug 17, 2023 at 12:37

1 Answer 1

0
$\begingroup$

Assuming classical logic and strong excluded middle, your proof goes like this.

Require Import Utf8 ClassicalEpsilon.

Section Equality_Dominance.

  Variable U : Set.
  Variable A B : U → Prop.
  Variable C : (U → nat) → Prop.

  Hypothesis Equality : ∀ f : U → nat, (∀ i : U, A i → f i = 0) → ¬ C f.

  Hypothesis Dominance : ∀ f : U → nat,
      (∀ i : U, B i → f i ≥ 0) → (∃ i : U, B i ∧ f i > 0) → C f.

  Theorem B_subset_A : ∀ i : U, B i → A i.
  Proof.
    set (f := (λ i : U, if (excluded_middle_informative (A i)) then 0 else 1)).
    assert (H : ¬ C f).
    { apply Equality.
      unfold f.
      intros i.
      destruct excluded_middle_informative; intuition. }
    intros i H0.
    apply NNPP.
    contradict H.
    apply Dominance.
    - intros j H1.
      unfold f.
      destruct excluded_middle_informative; intuition.
    - exists i.
      unfold f.
      destruct excluded_middle_informative; intuition.
  Qed.

End Equality_Dominance.

Print Assumptions B_subset_A.
$\endgroup$
2

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.