Can I avoid using Option A when I know that head cannot fail?

Question

I am quite new in the world of the ATP, but definitely very motivated. I am starting to deal with dependent types. I am involved in a project where I have defined the type for (finite and infinite) sequences.

Inductive sequence {X : Type} : Type :=
    | FinSeq (x : list X)
    | InfSeq (f : nat -> X). 

Now I want to define the head of a non-empty sequence.

Lemma aux_hd : forall {A : Type} (l : list A),
    0 < Datatypes.length l  -> @hd_error A l = None -> False.
Proof. destruct l.
 + simpl. lia. 
 + simpl. intros S. discriminate.
Qed.

Definition Hd {A : Type} (l : list A) : 0 < Datatypes.length l -> A :=
    match (hd_error l) with
    | Some a => (fun _ => a)
    | None => fun pf => match (aux_hd l pf ??) with end
    end.
     
Definition Head {A : Type} (s :sequence) (H : 0 << length s),
     match s with 
     | FinSeq x => Hd x H 
     | InfSeq f => f 0 end.

My problem is in the definition of Hd: I don't know how to prove @hd_error A l = None, since we are already in such a match branch. I believe it should be really easy.

I have a similar problem in the last definition because I don't know how to transform H, for the particular case of the first match branch, where I know that length s = Datatypes.length x and, thus, 0 << length s -> 0 < Datatypes.length x.

Finally, I have omitted the details about << and length sequence, because I dont think it is relevant for the question but basically I have uplifted nat with an Inf to represent the length of the infinite sequences and << is the < for nat and num.

I have followed the course Software Foundations and I am currently studying more using "Certified Programming with Dependent Types" which is also really good. Thanks in advance, Miguel

Answer 1

When you match on something, all extra evidence must be passed as arguments to the match (this is the "convoy pattern" described in CPDT).

In Hd you want to remember that hd_error l = None, pass it as an argument. It's a little tricky because you have to explicitly annotate the match with a return clause (which in simpler cases was inferred for you):

Definition Hd {A : Type} (l : list A) : 0 < Datatypes.length l -> A :=
    match (hd_error l) as X return hd_error l = X -> 0 < Datatypes.length l -> A with
    | Some a => (fun _ _ => a)
    | None => fun pf1 pf2 => match (aux_hd l pf2 pf1) with end
    end eq_refl.

Similarly in Head, after pattern-matching on s you want to simplify 0 << length s; pass it as an argument:

Definition Head {A : Type} (s :sequence) (H : 0 << length s) :=
     match s return (0 << length s) -> _ with 
     | FinSeq x => fun H => Hd x H 
     | InfSeq f => fun _ => f 0
     end H.