If two constructor expressions of an inductive type are equal in Coq, can I do rewriting based on their corresponding arguments?

user_14363423 0
Viewed 214

I do have a 4-tuple inductive type as follows:

Inductive my_tuple :=
  | abcd : byte -> nat -> byte -> nat -> my_tuple.

and in my context I do have the following:

H : abcd b1 n1 b2 n2 = abcd b1' n1' b2' n2'

Given the fact that all constructors for inductive types are injective and disjoint (also discussed here), I'm wondering if I can conclude the corresponding arguments are equal (i.e., b1 = b1', n1 = n1', b2 = b2', and n2 = n2') and then use them to rewrite other equations in my proof. If so, how can I do that? I have already seen these posts (here and there) but still couldn't figure out how to do so.

Thanks in advance for any comments.

coq-tactic coq formal-verification proof
1 Answers

Usually, injection is pretty simple, just Coq automation can solve most easy cases. For example in your case, the injection tactic is very straightforward.

Theorem Injective_tuple : forall b1 n1 b2 n2 b1' n1' b2' n2',
  abcd b1 n1 b2 n2 = abcd b1' n1' b2' n2' -> b1 = b1' /\ n1 = n1' /\ b2 = b2' /\ n2 = n2'.
  intros.
  injection H.
  intros.
  subst.
  do 4! constructor.
  Show Proof (*what actually coq is doing ? *).
Qed.

But I assume that you want to understand what is happening in the theorem above. In that case, well..., still pretty simple. You can look at the theorem generated by Coq, essentially is :

(* A not so beautiful proof *)
Definition Raw_Injective_tuple b1 n1 b2 n2 b1' n1' b2' n2' :
  abcd b1 n1 b2 n2 = abcd b1' n1' b2' n2' -> b1 = b1' /\ n1 = n1' /\ b2 = b2' /\ n2 = n2' :=
    fun H => 
      let first := (f_equal (fun x => match x with
                       |abcd x _ _ _ => x
                    end) H) in
       let second := (f_equal (fun x => match x with
                       |abcd _ x _ _ => x
                     end) H) in
       let three := (f_equal (fun x => match x with
                       |abcd _ _ x _ => x
                     end) H) in
       let four := (f_equal (fun x => match x with
                       |abcd _ _ _ x => x
                     end) H) in conj first (conj second (conj three four)).

f_equal or congruence (like Agda) is a theorem that says if you have a function you can apply in both sides of equality and it'll preserve the equal relation (x = y -> f x = f y). Well if you are able to extract the value of both sides of the equation, so the values are equal and the function injective, in that case by pattern matching was enough.

user_98204830
Related