7
$\begingroup$

I was messing around with toy lemmas in Idris and came up with this silly proof.

%default total

data Dumb : Nat -> Type where
  Way : Dumb Z
  NoWay : Dumb (S k) -> Dumb k

notDumb : Dumb (S k) -> Void
notDumb (NoWay d) = notDumb d

And in Agda...

data Dumb : ℕ -> Set where
  way : Dumb 0
  no_way : {k : ℕ} -> Dumb (suc k) -> Dumb k 

not_dumb : {k : ℕ} -> Dumb (suc k) -> ⊥
not_dumb (no_way d) = not_dumb d

Pretty straightforward. But then when I tried it in Coq, it became a bit tricky. The only way I could figure out how to do it was with dependent induction.

Require Import Coq.Program.Equality.

Inductive dumb: nat -> Prop :=
  | way : dumb 0
  | noway (k: nat): dumb (S k) -> dumb k.

Lemma not_dumb: forall k, ~dumb (S k).
Proof.
  intros. intro.
  dependent induction H.
  apply (IHdumb (S k)).
  auto.
Qed.

And the proof term is pretty complicated.

not_dumb = 
fun k : nat =>
(fun H : dumb (S k) =>
 (fun (gen_x : nat) (H0 : dumb gen_x) =>
  (fun H1 : dumb gen_x =>
   dumb_ind
     (fun gen_x0 : nat =>
      forall k0 : nat, gen_x0 = S k0 -> block (block False))
     (fun (k0 : nat) (H2 : 0 = S k0) =>
      False_ind (block (block False))
        (let H3 : False :=
           eq_ind 0
             (fun e : nat =>
              match e with
              | 0 => True
              | S _ => False
              end) I (S k0) H2 in
         False_ind False H3))
     (fun (k0 : nat) (H2 : dumb (S k0))
        (IHdumb : forall k1 : nat, S k0 = S k1 -> block (block False))
        (k1 : nat) (H3 : k0 = S k1) =>
      solution_left nat
        (fun x : nat =>
         dumb (S x) ->
         (forall k2 : nat, S x = S k2 -> block (block False)) ->
         block (block False)) (S k1)
        (fun (_ : dumb (S (S k1)))
           (IHdumb0 : forall k2 : nat,
                      S (S k1) = S k2 -> block (block False)) =>
         IHdumb0 (S k1) eq_refl : block False) k0 H3 H2 IHdumb) gen_x
     H1) H0 k) (S k) H eq_refl)
:
~ dumb (S k)
     : forall k : nat, ~ dumb (S k)

So the questions are:

  1. Why are these proofs so different? Is there something fundamental about languages like Idris and Agda which make this sort of proof simpler? Is there something about Coq that makes this kind of proof hard? My sense is it has something to do with pattern matching, but it would be great if someone who knows more about pattern matching in Idris or Agda could verify this.

  2. What's going on in this Coq proof? Is it ultimately doing the same thing as what is being done in the Idris/Agda case? Is it just that Coq's totality checker is doing less work?

  3. Is there actually a very simple Coq proof of this? And the entire issue is moot?

Thanks, anything helps.


Follow up. Thanks for the nice responses. They made me realize you can do this directly with the induction principle, albeit not using tactics.

Definition is_zero (n : nat) : Prop :=
  match n with
  | 0 => True
  | (S _) => False
  end.

Lemma dumb_is_zero : forall k, dumb (S k) -> is_zero (S k) -> is_zero k.
Proof.
  intros.
  destruct k.
  - exact I.
  - assumption.
Qed.

Lemma not_dumb: forall k, ~dumb (S k).
Proof.
  intros k d.
  exact (dumb_ind is_zero I dumb_is_zero (S k) d).
Qed.

I'm still curious though, is there any way of generating the proof using tactics?


I guess ultimately the point is that I really want to prove

Lemma not_dumb: forall k, dumb (S k) -> is_zero (S k).
Proof.
  intros k d.
  induction d.
  - exact I.
  - inversion IHd.
Qed.

Thanks again.

$\endgroup$
3
  • 1
    $\begingroup$ What I'd find interesting is, why does Agda's totality checker actually accept this? $\endgroup$ Nov 16, 2022 at 17:16
  • $\begingroup$ Agreed, I think this is why I sense this is in part about the totality checkers in Agda and Idris doing a lot of the work to make this clean. I think intuitively, the checker can tell the way pattern is unnecessary, and the noway pattern has a strictly smaller term on the right-hand side, so it is structurally sound. $\endgroup$
    – Nathan
    Nov 16, 2022 at 17:53
  • $\begingroup$ @leftaroundabout Such ability of totality checker is one the main points of GADTs/Indexed inductive types. $\endgroup$
    – uhbif19
    May 22, 2023 at 10:55

2 Answers 2

8
$\begingroup$

There is a coq proof which doesn't require dependent induction:

Lemma dumb0 : forall k, dumb k -> k = 0.
Proof.
  intros k dumb.
  induction dumb.
  - reflexivity.
  - discriminate IHdumb.
Qed.

Lemma not_dumb: forall k, ~dumb (S k).
Proof.
  intros k dumb.
  discriminate (dumb0 (S k) dumb).
Qed.

And a way to write the proof as a fixpoint, which looks very similar to the Idris and Agda examples:

Lemma false_succ_eq_zero : forall {P : Prop} {k : nat}, S k = 0 -> P.
Proof.
  discriminate.
Qed.

Fixpoint dumb0' {k : nat} (d : dumb k) : k = 0 :=
  match d with
  | way => eq_refl
  | noway k' d' => false_succ_eq_zero (dumb0' d')
  end.

Definition not_dumb' {k : nat} (d : dumb (S k)) : False :=
  false_succ_eq_zero (dumb0' d).

Notice how dumb0' has the same recursion scheme as notDumb and not_dumb in Idris and Agda.


However, there's a lot more boilerplate in the Coq version. And the latter proof is hiding some of the complexity in the false_succ_eq_zero term:

false_succ_eq_zero = 
fun (P : Prop) (k : nat) (H : S k = 0) =>
let H0 : False := eq_ind (S k) (fun e : nat => match e with
                                               | 0 => False
                                               | S _ => True
                                               end) I 0 H in
False_ind P H0

Coq proofs are "mechanized": they make heavy use of generalized tactics, which produce the ugly code that you see in the Print statements, but enable proof automation (ex: auto randomly tries a predefined set of tactics, lia solves arbitrary linear relations, the Ltac language lets you define custom tactics). Idris and Agda instead rely on more traditional pattern matching, thus their definitions are more "readable" (and there is no separate "proof buffer" in the interactive theorem-proving process) and their dependent type unification is stronger (see: Agda's cubical types, which supposedly automate a lot of "intuitive" things you must explicitly do with Coq like rewrite equalities), but they don't have the kind of powerful automation that Coq does.

$\endgroup$
1
  • $\begingroup$ Thanks for the nice coq proof! It made me realize that there is a very simple proof using dumb_ind directly. I'm still a bit curious if there is a way for this proof to be generated using tactics. Is this just a limitation of tactics? I think I understand generally that tactics have a way of producing ugly proof terms, but it seems unfortunate that they block obvious clean solutions. $\endgroup$
    – Nathan
    Nov 16, 2022 at 17:45
7
$\begingroup$

Additionally to the existing answer, there is also a way to use the same kind of pattern-matching facilities that Agda provides in Coq using the Equations library:

Inductive dumb: nat -> Prop :=
  | way : dumb 0
  | noway (k: nat): dumb (S k) -> dumb k.

From Equations Require Import Equations.

Equations not_dumb {n} (x : dumb (S n)) : False :=
  | noway k y := not_dumb y.

```
$\endgroup$
1
  • $\begingroup$ I really like this solution, I'll have to put this in my back pocket. It does hide a lot of the complexity, and does seem to indicate that it really is quite tricky to have a solution as clean in this in coq. $\endgroup$
    – Nathan
    Nov 16, 2022 at 17:59

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.