forall equality in Coq

Question

I am trying to prove the following equality:

Lemma Foo (A : Type) (n : nat) (gen : forall p : nat, p < S n -> A)
(ic0 : 0 < S n) (ic1 : 0 mod S n < S n):
  gen (n - n) ic1 = gen 0 ic0.

The n-n is 0 by Nat.sub_diag and 0 mod S n is also 0 by Nat.mod_0_l. However I could not easily apply these lemmas to types. I tried usual trick of remember/rewrite/subst but subst part fails:

   remember (gen (n-n)) as Q.
   remember (n-n) as Q1.
   rewrite Nat.sub_diag in HeqQ1.
   subst.

P.S. This question may use a better title. Please suggest.

I think the Coq library might have a proof of unicity of lt n m somewhere - and if not, I think I've seen it float by a couple times on coq-club so you might try searching the mailing list archives. Then, you could generalize ic0 and ic1 which should hopefully allow for the rewriting. — Daniel Schepler
not sure how to use unicity here. By the way, I am OK to use proof irrelevance, if that helps... — krokodil

Jason Gross Jason Gross · Accepted Answer · 2017-10-11T05:30:34

The subst tactic fails because remember is buggy; I have reported this bug here. (As a sanity, check, finishing a goal with abstract admit, where admit comes from Coq.Compat.AdmitAxiom, should never fail with a type error. If it does, that means there's a bug in Coq (or a plugin you're using).)

Here is a working proof (tested in 8.6.1 and 8.7+beta2):

Require Import Coq.Arith.Arith.

Lemma Foo (A : Type) (n : nat) (gen : forall p : nat, p < S n -> A)
      (ic0 : 0 < S n) (ic1 : 0 mod S n < S n):
  gen (n - n) ic1 = gen 0 ic0.
Proof.
  revert ic0 ic1; simpl; rewrite Nat.sub_diag; intros ic0 ic1.
  apply f_equal, le_unique.
Qed.

Note that you got lucky, in some sense, that n - n and 0 mod S n are judgmentally equal. Using simpl exposes this fact, and allows rewrite to work.

forall equality in Coq

1 Answers