Pattern match with two list whose type is dependent type on Coq

Question

I defined this function.

Inductive Euc:nat -> Type:=
|RO : Euc 0
|Rn : forall {n:nat}, R -> Euc n -> Euc (S n).

Notation "[ ]" := RO.
Infix ":::" := Rn (at level 60, right associativity).

Fixpoint QE {A}(b c:Euc A) :=
 match b,c with
 |b':::bs, c'::: cs => (b'+c') ::: QE bs cs
 |_, _ => []
 end.

I have encountered the error "The term "[]" has type "Euc 0" while it is expected to have type "Euc A" ".

How do I teach Coq that Euc 0 is Euc A?

Tiago Campos Tiago Campos · Accepted Answer · 2020-09-10T07:02:07

Coq doesn't know that the only pattern left is the "RO" constructor, therefore you're not able to return an empty Euc. To fix that just remove the _ and specialize the case :

Fixpoint QE {A}(b c:Euc A) : Euc A.
 refine (match b,c with
 |RO, RO => _
 |H => ????
 end).

That forces coq to understand that you're dealing with a specific constructor. Also, Coq always will instantiate new variables (Types not) of elimination, thus coq may complain that bs and cs have different indexes. The coq vectordef library has several examples of how to manage this. A first approach and more mature it is to use elimination schemes, notice you can destruct a non-zero vector using the head and last. For example :

Definition rect_euc {n : nat} (v : Euc (S n)) :
   forall (P : Euc (S n) -> Type) (H : forall ys a, P (a ::: ys)), P v.
refine (match v  with
    |@Rn _ _ _ => _
    |R0 => _
  end).
apply idProp.
intros; apply H.
Defined.

Now, you just have to use the scheme to destruct both vectors preserving the length of both :

Fixpoint QE (n : nat) {struct n} : Euc n -> Euc n -> Euc n :=
  match n as c return Euc c -> Euc c -> Euc c with
    | S m => fun a => 
     (@rect_euc _ a _ (fun xs x b =>
         (@rect_euc _ b _ (fun ys y => (x + y) ::: @QE m xs ys))))
    | 0 => fun xs ys => []
   end.

Alternatively you can use the coq tactics to remember that two indexes are equal :

Fixpoint QE' (n : nat) (b : Euc n) : Euc n -> Euc n.
refine (match b in Euc n return Euc n -> Euc n with
    |@Rn m x xs => _    
    |@RO => fun H => []
 end).

remember (S m).
intro H; destruct H as [| k y ys].
inversion Heqn0.
inversion Heqn0.
subst; exact ((x + y) ::: QE' _ xs ys).
Defined.

Pattern match with two list whose type is dependent type on Coq

1 Answers