I use tuple in mathcomp to define fixed-width bit-vectors as “n.-tuple bool”.
An inductive type value represents all possible values (a bit-vector of some width or an undefined value).
Two implementations (andv_program and andv_eq_rect) of bit-wise AND operation over value are defined.
Program is used in andv_program while eq_rect is used in andv_eq_rect to do type casting.
Then I want to prove some property about the bit-wise AND operation.
With andv_eq_rect, I can prove the lemma test_eq_rect.
However, with andv_program, the corresponding lemma test_program is failed to prove using the same proof technique.
When I do “case: (Nat.eq_dec n n)”, Coq returns the following error message:
Error:
Ltac call to "case (ssrcasearg) (ssrclauses)" failed.
Illegal application:
The term "andv_program_obligation_1" of type
"forall (v1 : value) (n1 : nat) (bs1 : n1.-tuple bool) (n2 : nat),
Vbools bs1 = v1 ->
let filtered_var := Nat.eq_dec n1 n2 in
forall wildcard' : n1 = n2, in_left = filtered_var -> n2 = n1"
cannot be applied to the terms
"Vbools bs1" : "value"
"n" : "nat"
"bs1" : "n.-tuple bool"
"n" : "nat"
"eq_refl" : "Vbools bs1 = Vbools bs1"
"wildcard'" : "n = n"
"Heq_anonymous" : "in_left = s"
The 7th term has type "in_left = s" which should be coercible to
"in_left = Nat.eq_dec n n".
Below is the Coq code.
From Coq Require Import Program Arith.
From mathcomp Require Import ssreflect tuple.
Definition map_tuple2 {A B C : Type} (f : A -> B -> C) {n} (ls1 : n.-tuple A) (ls2 : n.-tuple B) : n.-tuple C :=
map_tuple (fun e => f (fst e) (snd e)) (zip_tuple ls1 ls2).
Definition cast {A n m} (l : n.-tuple A) (pf : n = m) : m.-tuple A :=
eq_rect n (fun n : nat => n.-tuple A) l m pf.
Inductive value : Type :=
| Vbools : forall {n : nat}, n.-tuple bool -> value
| Vundef : value.
Program Definition andv_program (v1 v2 : value) : value :=
match v1, v2 with
| Vbools n1 bs1, Vbools n2 bs2 =>
match Nat.eq_dec n1 n2 with
| left _ => Vbools (map_tuple2 andb bs1 bs2)
| right _ => Vundef
end
| _, _ => Vundef
end.
Definition andv_eq_rect (v1 v2 : value) : value :=
match v1, v2 with
| Vbools n1 bs1, Vbools n2 bs2 =>
match Nat.eq_dec n1 n2 with
| left pf => Vbools (map_tuple2 andb (cast bs1 pf) bs2)
| right _ => Vundef
end
| _, _ => Vundef
end.
Lemma test_eq_rect :
forall n (bs1 bs2 : n.-tuple bool),
andv_eq_rect (Vbools bs1) (Vbools bs2) = Vbools (map_tuple2 andb bs1 bs2).
Proof.
move=> n bs1 bs2. rewrite /andv_eq_rect /=. case: (Nat.eq_dec n n).
- move=> pf. rewrite /cast. rewrite -eq_rect_eq. reflexivity.
- move=> H; apply: False_ind; apply: H; reflexivity.
Qed.
Lemma test_program :
forall n (bs1 bs2 : n.-tuple bool),
andv_program (Vbools bs1) (Vbools bs2) = Vbools (map_tuple2 andb bs1 bs2).
Proof.
move=> n bs1 bs2. rewrite /andv_program /=.
case: (Nat.eq_dec n n).
Qed.
Is it possible to finish the proof of test_program?