Generally Mapping Inequality through Unary Constructors

Using Coq
1

I’m very much new to automated theorem proving, so please feel free to point out anything especially gross that I’m doing. :slight_smile: I’m in a situation where I’m writing a bunch of tiny helper lemmas that prove that inequality maps through constructors. For instance, I have a constructor VInt that wraps around an integer and I write the following:

Lemma integer_not_equal_implies_vint_not_equal :
  forall z1 z2 : Z, z1 <> z2 -> VInt z1 <> VInt z2.
Proof.
  unfold not. intros. injection H0. apply H.
Qed.

This gets old very fast. I’m assuming there’s some way for me to make a polymorphic version of this, such as

Lemma inequality_preserved_by_unary_constructor :
  forall A B : Type,
  forall C : A -> B, forall a1 a2 : A,
  a1 <> a2 -> C a1 <> C a2.
Proof.
  unfold not. intros. injection H0. apply H.
Qed.

but this proof is invalid because we’ve lost the information that C is a constructor. At injection H0, we have the state

1 goal
A : Type
B : Type
C : A -> B
a1, a2 : A
H : a1 = a2 -> False
H0 : C a1 = C a2
______________________________________(1/1)
False

and we can’t proceed with injection H0 because C isn’t known to be injective.

So I would assume that the problem is my type A -> B, since it doesn’t convey any notion of injectivity. What is the correct way to express that this lemma only applies for constructors?

2

you can just do congruence, eg

Lemma test : forall z1 z2 : nat, z1 <> z2 -> Some z1 <> Some z2.
Proof.
  congruence.
Qed.

If you want to state a general form of the lemma, it applies to any injective function (it’s just the contrapositive of injectivity).

3

Thanks! I’m glad to learn about congruence. But yes: I’m trying to understand how to generalize the lemma. Being a beginner, my problem is that I don’t know how to indicate that C must be injective. Like… what’s the syntax for that?

4

There’s no specific syntax, you just say it is.

5

As for any coding, the cat can been skinned several ways, anyway I suppose a “canonical” way to approach it would be firstly to define what injective of a function means, then adding the injectivity to the assumptions of the theorem.

In practice, that would look like this (where the theorem becomes totally trivial, but of course that’s not the issue here):

Definition injective {A B : Type} (P : A -> B) : Prop :=
  forall a1 a2 : A, a1 <> a2 -> P a1 <> P a2.

Lemma inequality_preserved_by_injection :
  forall (A B : Type) (P : A -> B),
    injective P ->
    forall a1 a2 : A,
      a1 <> a2 -> P a1 <> P a2.
Proof.
  unfold injective, not.
  intros A B P L a1 a2 H HP.
  apply (L a1 a2).
  - apply H.
  - apply HP.
  (* This would in fact suffice:
  unfold injective.
  intros A B P L.
  apply L. *)
Qed.
6

Thanks for the detailed explanation. :slight_smile: I think I’m still trying to understand the boundary between the standard libraries and the things I’m expected to define myself. Your definition of injective makes sense to me, but

  1. would a constructor for an inductive data type automatically be recognized as injective like it is when writing e.g. injection H.?
  2. would injective things be compatible with the injection tactic?

The reason I was anticipating a specific type-oriented annotation was because I was trying to make uses of the lemma I was writing limited to taking inductive data type constructors as arguments.

Thanks again for the information! I don’t think I’d be finding my footing without this kind of interactive help. :slight_smile:

7

This is quickly getting above my head… :slight_smile:

  1. would a constructor for an inductive data type
    automatically be recognized as injective like it is
    when writing e.g. [injection H0]?

Yes, as in your initial example with VInt. The fact is in Coq inductive constructors are not functions, they don’t evaluate to some value, they are rather term builders, in that they literally belong to / constitute the representation of a term: and destruction works by pattern matching on (to begin with) the constructor literal name. – IOW, these are constructors in the functional programming sense, so lexical constructs, as opposed to constructors as operations in the imperative (OO) programming sense.

For more and possibly better explanations, here are a couple of links:
https://stackoverflow.com/questions/32662889/how-do-we-know-all-coq-constructors-are-injective-and-disjoint
https://stackoverflow.com/questions/43762312/are-constructors-in-the-plain-calculus-of-constructions-disjoint-and-injective

More formally: I cannot find a piece of documentation that explicitly says that inductive constructors are “injective and disjoint”, I take it to be sort of inscribed in the details of the calculus, and I suppose this would be the starting point (not for the fainthearted):
https://coq.inria.fr/refman/language/core/inductive.html#inductive-definitions

  1. would injective things be compatible with the injection tactic?

No, the injection tactic only applies with inductive constructors, as documented here:
https://coq.inria.fr/refman/proofs/writing-proofs/reasoning-inductives.html#coq:tacn.injection

OTOH, I suppose you could write your own tactic, e.g. in Ltac, that leverages an available injectivity hypothesis. (Maybe congruence is already it? I am not sure: my point here just is that you can even write your own tactics…)

The reason I was anticipating a specific type-oriented annotation

There are several ways in Coq to approach what I’d lump under “sub-typing”, as well as quite some literature/articles on just that problem: from the top of my head, beside explicit assumptions, some kind of “sigma types” (maybe), modules, records, type classes… and I am far from an expert on any of that, so I’ll just leave it at some keywords.

But if you are new to Coq, IMHO you might be looking too far ahead already, especially considering that (with no exception, as far as I know) whatever more concise there is to express a concept, that concept can always be expressed using / be unfold back to the basic calculus, where its “ultimate meaning” really resides… whence also IMO the importance of not skipping that step in one’s learning.

I’ll close here by mentioning what I believe is a great resource for the practitioner beginning with Coq, the Software Foundations series, I’d say the first book at least:
https://softwarefoundations.cis.upenn.edu

And, for an even gentler introduction, here is a (relatively recent) series of videos that goes with the first chapters of that first book, by Prof. Michael Clarkson:
https://youtube.com/playlist?list=PLre5AT9JnKShFK9l9HYzkZugkJSsXioFs&si=xq6h9cqETxzB2aJe

8

Thanks for the thorough description! I agree that it’s crucial to work with the building blocks and not skip any steps. (I’m only a few days into this and I haven’t the faintest idea what auto does, but I’m not in a hurry to learn because I figure I should understand the tools it would apply for me.) The learning exercise I’ve chosen for myself is a proof of soundness for a little λ-calculus equipped with a handful of first-order operations and so it started to get pretty tedious to reprove the same lemmas for each different inductive type. :slight_smile: (That said, I’ve encountered a new challenge: how to write this proof for a pair of mutually defined types. This’ll be fun!)

I also appreciate the links you’ve provided. I’ve generally enforced a policy of not posting a question until I’m pretty sure it’s not out there on the 'net somewhere, but it’s challenging to be thorough when one doesn’t know all of the terminology.

In any case: my appreciation again for the lengthy responses! This has been informative and indispensable. :slight_smile:

1 Like