Failed to do case analysis with dependent type and Program used

Using Rocq
1

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?

2

Using Program in this definition does introduce an abstraction on the equality which is indeed quite difficult to handle, in order to destruct you will have to prove a more general lemma as I think no abstraction of Nat.eq_dec will satisfy the resulting Program term.

Moreover, using Program for this is quite overkill. I’d use a more idiomatic version of your eq_rect function:

Definition andv_eq_rect (v1 v2 : value) : value :=
  match v1, v2 with
  | Vbools n1 bs1, Vbools n2 bs2 =>
    match @eqP _ n1 n2 with
    | ReflectT pf => Vbools (map_tuple2 andb (cast bs1 pf) bs2)
    | ReflectF _ => Vundef
    end
  | _, _ => Vundef
  end.

Lemma test_eq_rect n (bs1 bs2 : n.-tuple bool) :
    andv_eq_rect (Vbools bs1) (Vbools bs2) = Vbools (map_tuple2 andb bs1 bs2).
Proof. by rewrite /andv_eq_rect /=; case: eqP => // eq; rewrite eq_axiomK. Qed.

but even better, in the case of tuples, which have an injection to list, I’d just use the base, non-dependently typed equality:

Definition ands (s t : seq bool) := map (prod_curry andb) (zip s t).
Definition andt n (s t : n.-tuple bool) := [tuple of ands s t].

Lemma test_program' n (bs1 bs2 : n.-tuple bool) :
  map_tuple2 andb bs1 bs2 = andt bs1 bs2.
Proof. by apply/val_inj/eq_in_map => -[b1 b2]. Qed.

You can see more of this style of programming at

3

Hi,

Thank you for the answer and the reference. I think I will learn more from the ssrbit library.