How do we know that all Coq constructors are injective and disjoint?
According to this course , all constructors (for inductive types) are injective and do not overlap:
... Similar principles apply to all inductively defined types: all constructors are injective, and the values constructed from different constructors are never equal. For lists, the constructor cons is injective and nil is different from every non-empty list. For booleans, true and false are not equal.
(And tactics inversion
based on this assumption)
I'm just wondering how do we know this assumption is the case?
As we know that, for example, we cannot determine natural numbers based on
1) Successor and possibly constructor "Double":
Inductive num: Type :=
| O : num
| S : num -> num
| D : num -> num.
and
2) some function plus
so that the same number 2
can be reached via two different constructor sequences / routes, S (S O)
and D (S O)
?
What mechanism in Coq that provides above will never happen?
PS I am not suggesting the above example num
is possible. I'm just wondering what makes it impossible.
thank
source to share
When you define an inductive data type in Coq, you are essentially defining a tree type. Each constructor gives the kind of node that is allowed to appear in your tree, and its arguments define the children and elements that the node can have. Finally, functions defined by inductive types (with the propositionmatch
) can check constructors that were used to obtain a value of this type in arbitrary ways. This makes Coq constructors very different from, for example, the constructors you see in OO. A constructor object is implemented as a regular function that initializes a value of a given type; Coq's constructors, on the other hand, are enumerating the possible values that our type's representation allows. To better understand this difference, we can compare the different functions that we can define on an object in traditional OO language and on an inductive type element in Coq. Let's use your example num
. Here's an object oriented definition:
class Num {
int val;
private Num(int v) {
this.val = v;
}
/* These are the three "constructors", even though they
wouldn't correspond to what is called a "constructor" in
Java, for instance */
public static zero() {
return new Num(0);
}
public static succ(Num n) {
return new Num(n.val + 1);
}
public static doub(Num n) {
return new Num(2 * n.val);
}
}
And here's the definition in Coq:
Inductive num : Type :=
| zero : num
| succ : num -> num
| doub : num -> num.
In the OO example, when we write a function that takes an num
argument, there is no way to know which "constructor" was used for that value, since this information is not stored in
val
. In particular, Num.doub(Num.succ(Num.zero()))
it
Num.succ(Num.succ(Num.zero()))
will be equal.
In the Coq example, on the other hand, things change because we can determine which constructor was used to generate the value num
thanks to the operator match
. For example, using Coq strings, we could write a function like this:
Require Import Coq.Strings.String.
Open Scope string_scope.
Definition cons_name (n : num) : string :=
match n with
| zero => "zero"
| succ _ => "succ"
| doub _ => "doub"
end.
In particular, although the value of your intention for designers means succ (succ zero)
and doub (succ zero)
must be "moral" equal, we can distinguish them by using cons_name
them:
Compute cons_name (doub (succ zero)). (* ==> "doub" *)
Compute cons_name (succ (succ zero)). (* ==> "succ" *)
In fact, we can use match
to differentiate succ
and in doub
an arbitrary way:
match n with
| zero => false
| succ _ => false
| doub _ => true
end
Now a = b
in Coq means there is no possible way that we can distinguish between a
and b
. The above examples show why doub
(succ zero)
and succ (succ zero)
cannot be equal, since we can write functions that do not respect the meaning we had in mind when we wrote this type.
This explains why the constructors do not overlap. That they are injective is also a consequence of pattern matching. For example, suppose we wanted to prove the following statement:
forall n m, succ n = succ m -> n = m
We can start the proof with
intros n m H.
Let's lead us to
n, m : num H : succ n = succ m =============================== n = m
Note that this goal is a simplification equivalent to
n, m : num
H : succ n = succ m
===============================
match succ n with
| succ n' => n' = m
| _ => True
end
If rewrite H
, we get
n, m : num
H : succ n = succ m
===============================
match succ m with
| succ n' => n' = m
| _ => True
end
which simplifies to
n, m : num H : succ n = succ m =============================== m = m
At this point, we can conclude with reflexivity. This method is pretty generic, and actually underlies what it does inversion
.
source to share