Brute Force, Formalized (V2)

Library fin_em2

Today I try to formalize the basic intuition that excluded middle is constructively true when we're working with finite types. I will prove a "brute force" theorem which says that we can determine the truth of a predicate by testing it over all values.

Through proofs-as-programs (aka Curry-Howard aka BHK corresponedence aka many other things), this is also a brute force program! This is why I use Defined instead of Qed and sig (subset types) instead of ∃. It really does work, as I will demonstrate after proving the theorem. Actually, the first version of the proof had a curious peculiarity: even after finding a counterexample, it would keep going and try to find the largest counterexample. If you move around the destruct in the theorem statement for em, you can recreate this maximum-counterexample program! Just one fun way in which choice of proof can become "relevant".

I eventually prove the theorem for a representative finite set type, and then show that it extends to any type isomorphic to a finite set type. This is used to give the theorem for Fin.t, which is used e.g. in Vector and thus somewhat unavoidable.

Require Import Setoid Program.
Require Import Arith Utf8 CpdtTactics Decidable Compare_dec List Bool.
Require Fin.
Set Implicit Arguments.

Fixpoint factorial n :=
  match n with
    | 0 => 1
    | (S pn) => n * factorial pn
  end.
Print factorial.

Section em.
  Hypothesis P : nat → Prop.

  Lemma forall_extends:
    ∀ n, (∀ x : nat, x < n → P x)
         → P n
         → (∀ x : nat, x < S n → P x).
    intros ? ? ? ? x_lt_S_n; inversion x_lt_S_n; crush.
  Defined.
  Hint Resolve forall_extends.

  Lemma sig_extends:
    ∀ n (base : {x : nat | x < n ∧ (P x → False)}),
      {x : nat | x < S n ∧ (P x → False)}.
    intros; destruct base as (?,(?,?)); eauto.
  Defined.
  Hint Resolve sig_extends.

Since we want an efficient algorithm, we are a little careful in this proof: we make sure we only compute (d x) if we have to, so we destruct the induction hypothesis earlier to see if we already have a counterexample.

  Theorem em :
    ∀ n (d : ∀ x, x < n → (P x) + ~ (P x)),
      (∀ x, x < n → P x) + {x | x < n ∧ ~ P x}.
    intros.
    induction n. intuition.
    assert (H : (∀ x : nat, x < n → P x) + {x | x < n ∧ (P x → False)}) by eauto.
    destruct H; eauto.
    destruct (d n); intuition eauto.
  Defined.
  Hint Resolve em.
End em.
Extraction em.

Let's demonstrate the power of our program!

Definition P1 x := x ≠ 2.
Hint Unfold P1.
Lemma d_P1 : ∀ n x, x < n → (P1 x) + ~ (P1 x).
intros.
pose proof (eq_nat_dec x 2).
intuition.
Defined.
Eval vm_compute in (em P1 (d_P1 (n := 5))).

Okay that was not very exciting. I found some better facts here: http://www2.stetson.edu/~efriedma/numbers.html . On this page it says that n=863 gives n(n + 6) a palindrome. Are there medium-size (>1) numbers that also satisfy this constraint? Let's find out!

First we must quickly hack up a way to represent decimal numbers, since we really meant a base-10 palindrome. We represent e.g. 123 as 3,2,1.

Definition number_stream_10 := list nat.

Fixpoint inc (n : number_stream_10) :=
  match n with
    | [] => 1 :: []
    | cons digit ds =>
      match lt_dec digit 9 with
        | left _ => (digit + 1) :: ds
        | right _ => 0 :: (inc ds)
      end
  end.
Fixpoint to_number_stream_10 x :=
  match x with
    | 0 => []
    | S px => inc (to_number_stream_10 px)
  end.

To test what we have so far: Compute (to_number_stream_10 12). It gave me 2; 1, so I probably haven't messed up yet.

Lemma dec_eq10 (a b : number_stream_10) : {a = b} + {a ≠ b}.
  refine (list_eq_dec _ a b).
  intros.
  pose proof (eq_nat_dec x y).
  intuition.
Defined.

Fixpoint palindrome' (front rear : number_stream_10): bool :=
  match front with
    | [] => if dec_eq10 rear (nil (A := nat))
            then true else false
    | b :: bs =>
      (if dec_eq10 bs rear then true else false) || (palindrome' bs (b :: rear))
  end.

To test what we have so far, I tried: Compute (palindrome' (to_number_stream_10 333)) ☐. It also really did work. Now we can define what we were really interested in: this is the predicate P2.

Definition palindrome n := palindrome' (to_number_stream_10 n) [] = true.
Definition P2 n := ¬ (palindrome (n * (n + 6)) ∧ n ≠ 0 ∧ n ≠ 1).
Lemma d_palindrome : ∀ n x, x < n → (P2 x + ~ P2 x).
intros.
unfold P2.
unfold palindrome.
destruct (eq_nat_dec x 1). intuition.
destruct (eq_nat_dec x 0). intuition.
destruct (palindrome' (to_number_stream_10 (x * (x + 6))) []); intuition.
Defined.

If you look at the output of this, you find 22 (the proof term is actually quite small and reasonable). It really does work! Note using vm_compute is definitely the way to go here, it is much faster than others!

Eval vm_compute in (em P2 (d_palindrome (n := 1000))).
Extraction em.

Our next section is a bit of a fight in math-bureaucracy, fighting to get the pretty result that deciding predicates over a finite type (Finite n) is decidable. In the end we do succeed to get our desired statement!

This is in many ways easier to use than the normal dependent Fin.t n datatype. But without some form of the (axiom-requiring) lemma below, we would have some issues with the second field not being irrelevant.

Definition Finite n := {x : nat | x < n}.
Hint Unfold Finite.
Definition finite x n (prf : x < n) : Finite n
  := exist (λ y : nat, y < n) x prf.

Local propositional irrelevance. By using dependent destruction, we bring in Axiom K and JMeq -> normal equality (Print Assumptions irr). Just adopting proof irrelevance would have worked fine too.

Lemma irr : ∀ m n (p1 p2 : m < n), p1 = p2.
  induction n; intuition.
  dependent destruction p1; dependent destruction p2; intuition.
  assert (p1 = p2); crush.
Qed.

Hint Rewrite irr.
Hint Resolve irr.

This tactic uses irrelevance to identify all terms of the same (a < b) type. This actually would be unecessary if the lemmas used computed, but they are marked by Qed.

Ltac auto_irr :=
  match goal with
    | [ |- context[?a]] =>
      match (type of a) with
        | (_ < _) =>
          match goal with
            | [ |- context[?b]] =>
              match (type of b) with
                | (_ < _) =>
                  rewrite (irr a b)
              end
          end
      end
  end; try trivial.

Section finite_em.
  Hypothesis n : nat.
  Hypothesis P : Finite n → Prop.
  Hypothesis d : ∀ x, (P x) + (~ P x).

We need to craft these predicates into the form that em wants them, starting with P.

  Definition P' x :=
    match lt_dec x n with
        | left is_lt => P (finite is_lt)
        | right _ => False
    end.

  Ltac simplP' :=
    match goal with
      | |- context[P' ?y] =>
        unfold P';
          destruct (lt_dec y _)
      | [ H : context[P' ?y] |- _ ] =>
        unfold P' in H;
          destruct (lt_dec y _)
    end.
  Ltac hyp_irr :=
    match goal with
      | [ lt1 : ?a < ?b, lt2 : ?a < ?b |- _ ] =>
        cut (lt1 = lt2); crush
    end.

  Lemma P_to_P' : ∀ x, P x → P' (proj1_sig x).
    intros.
    destruct x; simplP'; solve [auto] || hyp_irr.
  Defined.
  Hint Resolve P_to_P'.

  Lemma P'_to_P : ∀ (x : Finite n), P' (proj1_sig x) → P x.
    intros.
    destruct x; simplP'; solve [crush] || hyp_irr.
  Defined.
  Hint Resolve P'_to_P.

  Lemma d' (x : nat) (is_lt : x < n): (P' x) + (~ P' x).
    simplP'; crush.
  Defined.

  Lemma finite_1 :
    (∀ x : nat, x < n → P' x) → (∀ x : Finite n, P x).
    destruct x; auto.
  Defined.
  Hint Resolve finite_1.

  Lemma finite_2 : {x | x < n ∧ ~P' x} → {y | ¬P y}.
    intro ex; destruct ex as (x,(x_lt_n, not_P'_x)); intuition.
    exists (finite x_lt_n).
    intro P_y; exact (not_P'_x (P_to_P' P_y)).
  Defined.
  Hint Resolve finite_2.

  Theorem finite_em : (∀ x, P x) + {x | ~ P x}.
    destruct (em P' d'); crush; eauto.
  Defined.
  Hint Resolve finite_em.
  Hint Immediate finite_em.
End finite_em.

Section generalized_em.
  Hypothesis T : Type.
  Hypothesis P : T → Prop.
  Hypothesis n : nat.
  Hypothesis intoFinite : T → Finite n.
  Hypothesis intoT : Finite n → T.
  Hypothesis T_id : ∀ x, (intoFinite ∘ intoT) x = x.
  Hypothesis Finite_id : ∀ x, (intoT ∘ intoFinite) x = x.
  Hypothesis d : ∀ x, (P x) + (~ P x).

  Definition PF x := P (intoT x).
  Hint Unfold PF.
  Lemma dF : ∀ x, (PF x) + (~ PF x).
    eauto.
  Defined.
  Hint Resolve dF.
  Lemma pF : (∀ x, PF x) + {x | ~ PF x}.
    apply finite_em.
    eauto.
  Defined.
  Hint Resolve pF.
  Lemma generalized_em : (∀ x, P x) + {x | ~ P x}.
    destruct pF; unfold PF in *.
    - left. intro.
      rewrite <- Finite_id.
      eauto.
    - right.
      destruct s.
      eauto.
  Defined.
End generalized_em.

Definition FiniteFromFin (n : nat) (t : Fin.t n): Finite n :=
  Fin.to_nat t.
Hint Unfold FiniteFromFin.
Definition FinFromFinite (n : nat) (t : Finite n) :=
  match t with
    | exist x xltn => Fin.of_nat_lt xltn
  end.
Hint Unfold FinFromFinite.

Lemma Fin_id : ∀ n (x : Fin.t n), FinFromFinite (FiniteFromFin x) = x.
  intros.
  induction x; trivial.
  unfold FiniteFromFin in *.
  unfold FinFromFinite in *.
  unfold Fin.to_nat.
  fold @Fin.to_nat.
  destruct (Fin.to_nat x).
  crush.
  auto_irr.
Defined.

Lemma Finite_id: ∀ n (x : Finite n), FiniteFromFin (FinFromFinite x) = x.
induction n.
- destruct x. inversion l.
- destruct x; destruct x; simpl.
  + auto_irr.
  + fold (FinFromFinite (exist _ x (lt_S_n x n l))).
    rewrite IHn.
    auto_irr.
Defined.

やった！

Playing with Partiality in Coq

Library partial

It's well known (or at least it should be), that though coq is a total functional programming langauge, that doesn't stop us from expressing our computations in it. The partiality monad (see e.g. Operational Semantics Using the Partiality Monad) is a pretty natural and enjoyable way to do this.

This work is heavily inspired by the cpdt chapter on streams in its technique: especially the useful trick of manually writing the coinduction predicate. There is actually a brief mention of this monad in cpdt, with a demonstration of its inconveniences. You can see there for that, but for now lets keep the parade sunny --- we won't have any problems in this development.

The actual examples here come from Aaron Stump's blog; I wrote them up in agda earlier using the standard library (http://hpaste.org/78532), but today I actually develop the partiality monad from scratch for them.

Why coq now? Partly for learning, but also it seems to me that proper coinduction (see later, Park's principle) is often a very pretty way to present proofs. However it generates many small and tedious goals which proper automation can dispose of (but would be hell to write manually).

Require Import Setoid.
Require Import Arith Utf8 CpdtTactics List.
Set Implicit Arguments.

A partial value can be thought of as a computation which takes time to run. The actual return value is of the form (now x). For every "unit" of time it took to compute, there is a "later" constructor wrapped around (now x). I write "unit" in quotes because there is actually no requirement that the units of time have any relationship to real-world time.

To analyze partial values, I invent current and future. Once a computation returns, its future is constant --- always the final value.

CoInductive Partial (A : Type) : Type :=
| now : A → Partial A
| later : Partial A → Partial A.

Hint Constructors Partial.

Definition current {A : Type} (x : Partial A) :=
  match x with
    | now x' => Some x'
    | later x' => None
  end.

Definition future {A : Type} (x : Partial A) :=
  match x with
    | now x' => now x'
    | later x' => x'
  end.

Fixpoint future_at {A : Type} n (x : Partial A) :=
  match n with
    | 0 => x
    | S m => future (future_at m x)
  end.

CoFixpoint never (A : Type): Partial A := later (never A).

Coq is extremely cautious when it comes to expanding out coinductive computations, since it doesn't want to loop forever. If we have a coinductive value x, and we rewrite it to the form matchAndDoNothing x, coq will be willing compute the first entry in x for the pattern match. In general, it will expand out only so much of the stream that is actually "used" (as far as I know, this is equivalent to being pattern matched on --- there are no other elimination forms).

Definition matchAndDoNothing {A : Type} (P : Partial A) :=
  match P with
      | now x => now x
      | later y => later y
  end.
Lemma xisx (A : Type) (x : Partial A): x = matchAndDoNothing x.
destruct x; auto.
Qed.

A tactic for tearing apart existentials and conjunctions, since intuition won't do it for us.

Ltac destruct_conj :=
  repeat (
  match goal with
      | [H : (_ ∧ _) |- _] => destruct H
      | [H : prod _ _ |- _] => destruct H
      | [H : ∃ _, _ |- _] => destruct H
  end).

The crush tactic is normally hopeless when it comes to proving existentials, because it won't try to guess which value x to use for exists x, P(x). Sometimes we can hack around this by throwing around a bunch of unknown "existential values" (instantiating x with a ?) and hoping that the ? gets filled. This tactic is often stupid compared to eauto, but it happens to work well enough today.

Ltac ecrush :=
  try (match goal with
      | [ |- ∃ _, _ ] =>
        try solve [eexists; ecrush]
      | [ |- _ ∨ _ ] =>
        try (solve [eleft; ecrush]
                   || solve [eright; ecrush])
      | _ => solve [crush]
  end).

A special tactic for dealing with coinduction proofs where we need to extract info from an existential coinductive variable. A bit of a hack to call destruct_conj, in order to clean up the internals as quickly as possible. In general I'm not being very careful with my tactics, and they have unintended side-effects --- but for just this development it doesn't really matter.

Ltac destruct_exists :=
  try (match goal with
      | [H : ∃ _, _ |- _] =>
        let x := fresh "x"
        with Hx := fresh "Hx"
        in destruct H as (x, Hx);
           destruct_conj;
           destruct x
  end).

A tactic which wraps around aforementioned neverisnever hack to force computation in coinductive types.

Ltac simpl_co x :=
  rewrite (xisx x); simpl;
  try (match goal with
    | [|- context[match ?P with
                   | now x => now x
                   | later y => later y
                 end]]
=> (fold (matchAndDoNothing P); rewrite <- xisx)
  end).

Now that all the useful tactics are declared, back to the actual content. It's not called the partiality monad for nothing.

CoFixpoint bind {A B : Type} (x : Partial A) (f : A → Partial B): Partial B :=
  match x with
    | now x => f x
    | later x => later (bind x f)
  end.

Notation "x >>= f" := (bind x f) (at level 42).

Lemma bind_unit : ∀ A B (a : A) (f : A → Partial B), (now a) >>= f = f a.
intros; simpl_co (now a >>= f); trivial.
Qed.

Hint Rewrite bind_unit.

Equality of partial values (formally, strong bisimulation). Unfortunately, without extensionality = is pretty undesirable for coinductive values; you have to define values the same way for them to be intensionally equal.

CoInductive PEq (A : Type) : Partial A → Partial A → Prop :=
  | wnow : ∀ (x y : A), PEq (now x) (now x)
  | wlater : ∀ x y, PEq x y → PEq (later x) (later y).

Hint Constructors PEq.

Simplify the arguments to Bisimilarity. This is easy to write in terms of simpl_co. For some silly reason I decided I would try to make it more hygienic in its side-effects, which in the end didn't help anybody (and it's still not really hygienic).

Ltac simpl_under_PEq :=
  match goal with
    | [|- PEq ?A ?B] =>
      rewrite (xisx A); simpl;
      rewrite (xisx B); simpl;
      try (match goal with
               | [|- PEq (match ?P with
                                     | now x => now x
                                     | later y => later y
                                   end) _]
                 => fold (matchAndDoNothing P); rewrite <- xisx
                 end);
      try (match goal with
             | [|- PEq _ (match ?Q with
                                  | now x => now x
                                  | later y => later y
                                end)]
               => fold (matchAndDoNothing Q); rewrite <- xisx
                 end)
  end.

Strong bisimulation is an equivalence relation.

Lemma PEq_refl : ∀ {A : Type} (a : Partial A), PEq a a.
cofix. intros.
destruct a; constructor; auto.
Qed.

Hint Resolve PEq_refl.

Lemma PEq_trans: ∀ A (a b c : Partial A), PEq a b → PEq b c → PEq a c.
cofix.
intros.
inversion H; inversion H0; crush.
constructor.
eauto.
Qed.


Lemma PEq_symm : ∀ A (a b : Partial A), PEq a b → PEq b a.
cofix. intros.
inversion H; constructor; eauto.
Qed.

Hint Resolve PEq_symm.

Add Parametric Relation A : (Partial A) (PEq (A:=A))
  reflexivity proved by PEq_refl
  symmetry proved by (PEq_symm (A := A))
  transitivity proved by (PEq_trans (A := A))
    as PEq_rel.

This is the exciting part. Up to now we've been writing proofs with cofix, which is okay but not great: it's very easy to write a good-looking proof and have it get rejected due to guardedness (coq needs to see that the proof "produces" something eventually; see e.g. cpdt if you need background). Automation tools have a big problem with this, since circular proofs are very short and thus easy to compute. Instead of using that ugly jaunt, we will use a proper coinduction predicate.

I think of coinduction in terms of invariants. In order to prove equality, we choose a "bisimulation" R --- basically, an invariant stronger than equality. This invariant is preserved when we step forward in time --- that is to say, when we apply future to both of our arguments (see h2). R (see h1) implies that our immediate observation (current) of the computations is identical; because it is always preserved, there is never a way to tell the streams apart. If we have the base case, that R holds at time zero (for our initial arguments; unnamed and final hypothesis) then we can use this information to construct a value of type PEq.

That was a relatively complete explanation, but here's something simpler. Just looking at h1 and h2, we see that current (future_at n p1) = current (future_at n p2) for all n. We want to choose a predicate R which explains why this crucial equation is true, by proving h1 and h2. Looking at our examples later, this intuition should hopefully crystallize.

The coinduction principle is sometimes referred to as Park's principle.

Section PEq_coind.
  Variable A : Type.
  Variable R : Partial A → Partial A → Prop.
  Hypothesis h1 : ∀ p1 p2, R p1 p2 → current p1 = current p2.
  Hypothesis h2 : ∀ p1 p2, R p1 p2 → R (future p1) (future p2).

  Lemma Simple_Bisim1 : ∀ a b, R (now a) b → PEq (now a) b.
    intros. apply h1 in H. destruct b; crush.
  Qed.

  Lemma Simple_Bisim2 : ∀ a b, R (later a) (now b)
                               → PEq (later a) (now b).
    intros; apply h1 in H; crush.
  Qed.

  Theorem PEq_coind : ∀ p1 p2, R p1 p2 → PEq p1 p2.
  cofix. destruct p1.
  - apply Simple_Bisim1.
  - destruct p2.
    + apply Simple_Bisim2.
    + intros. constructor.
      assert (Heq := h2 H); apply PEq_coind; trivial.
  Qed.
End PEq_coind.

Lemma neverIsNever A : PEq (never A) (never A).
apply (PEq_coind (λ p1 p2, p1 = never A /\ p2 = never A)); crush.
Qed.

I will demonstrate a very simple coinductive proof using plus first.

Definition plus (a b : Partial nat) :=
  a >>= λ a', b >>= λ b',
  now (a' + b').

Hint Rewrite plus_0_r.

Lemma plusNowIsAdd : ∀ x y, plus (now x) (now y) = now (x + y).
  unfold plus; crush.
Qed.

Hint Rewrite plusNowIsAdd.
Hint Resolve now.

Coinduction generates a large number of subgoals (the hypotheses from before). If we choose our predicate right, they are often relatively trivial --- then coind_forceful can dispose of them completely.

Ltac coind_forceful P :=
  apply (PEq_coind P);
  intuition; destruct_exists; ecrush.

Demonstration! Remember that the coinductive predicate is all that really matters. y here is future_at n x where n represents the current time. p1 and p2 are similarly future_at n x and future_at n (plus x (now 0)).

Here is my "intuitive" explanation: y represents the current state of the computation x. Both of our computations wait for y to terminate, so they are equal up to that point. Once y does terminate, the proof is also trivial.

Theorem zeroAdd : ∀ (x : Partial nat), PEq x (plus x (now 0)).
intros. coind_forceful (λ p1 p2, ∃ y, p1 = y ∧ p2 = plus y (now 0)).
Qed.

We can prove very useful and seemingly scary theorems by just choosing the right coinductive predicates. In this case, we step-by-step observe the evolution of a --- once it actually returns a value x then we are left with b x >>= c on both sides and it is obvious they are equal from then on.

Lemma bind_assoc : ∀ A B C (a : Partial A)
                     (b : A → Partial B)
                     (c : B → Partial C),
                     PEq ((a >>= b) >>= c) (a >>= (λ x, b x >>= c)).
intros.
coind_forceful (λ p1 p2,
                (∃ y, p1 = (y >>= b) >>= c ∧ p2 = y >>= (λ x, b x >>= c))
                  ∨
                (p1 = p2)).
Qed.
Hint Resolve bind_assoc.

Lemma PEq_current : ∀ A (p1 p2 : Partial A), PEq p1 p2
                                             → current p1 = current p2.
intros.
destruct p1; destruct p2; inversion H; crush.
Qed.

Lemma PEq_future : ∀ A (p1 p2 : Partial A), PEq p1 p2
                                            → PEq (future p1) (future p2).
intros.
destruct p1; destruct p2; inversion H; crush.
Qed.

Hint Resolve PEq_current PEq_future.

The proof here is much like those before --- how pretty!

Lemma bind_cong : ∀ (α β : Type) (f g : α → Partial β),
                    (∀ (x : α), PEq (f x) (g x)) →
                    ∀ (x : Partial α), PEq (x >>= f) (x >>= g).
intros.
coind_forceful (λ p1 p2,
                PEq p1 p2 ∨ (∃ y, p1 = (y >>= f) ∧ p2 = (y >>= g))).
Qed.

Hint Resolve bind_cong.

A "real" demonstration. In fact there is no coinduction in this development, since we already wrote cong and assoc (which crush will call upon). This is quite a satisfying end, however.

Section RevMap.
  Hypothesis α β : Type.
  Hypothesis f : α → Partial β.
  Fixpoint revmap (l : list α) (l' : list β): Partial (list β) :=
    match l with
      | nil => now l'
      | x :: l => f x >>= λ f_x, revmap l (f_x :: l')
    end.

  Theorem revmapsplits :
    ∀ (l1 l2 : list α) (l' : list β),
      PEq (revmap (l1 ++ l2) l') (revmap l1 l' >>= revmap l2).
    induction l1 as [|x]; crush.
    destruct (f x) as [|p]; crush.

    simpl_under_PEq; constructor.
    transitivity (p >>= (λ f_x : β, revmap l1 (f_x :: l') >>= revmap l2)); auto.
  Qed.
End RevMap.

This blog actually begins

It is very convenient that I have already setup a blog. The first post was not even that bad, after some editing! Or so I think. Anyway, now I will finally start posting some content. As proof I know how to use a blog, I will figure out how to use latex! \[ \DeclareMathOperator{\Set}{Set} \DeclareMathOperator{\suc}{suc} \DeclareMathOperator{\Id}{Id} \DeclareMathOperator{\refl}{refl} \DeclareMathOperator{\Cong}{cong} \DeclareMathOperator{\prf}{prf} J : \prod(A : \Set) (P : \Pi(x\ y : A) (I : \Id x\ y), \Set), \\ (\Pi(a : A), P(a,a,\refl A a)) \to (\Pi(x\ y : A)(i : \Id x\ y), P\ x\ y\ i) \] This is the glorious induction principle for equality in dependent type theory. More on this later!