The Coq mailing list

[Holden Lee <holdenlee AT alum.mit.edu>]

I'm working on defining sums over finite sets. Sparing the details, it goes like this

Variable T : finType.

Definition foldmap 

  {U:Type} (f: U -> U -> U) (g: T-> U) (start: U) (A: {set T}) : U.

...

Definition sums

  (A: {set T}) (g: T -> nat) : nat :=

  foldmap (fun a b => a + b) g 0 A.

Lemma sum0:

  forall g, sums set0 g = 0.

Proof.

  intro g. unfold sums. unfold foldmap. 

At this point, the goal looks like (basically, foldmap is defined by recursing on the cardinality of A; here choosing' H gives { x:T | x \in A /\ n = #|A :\ x| /\...})

g : T -> nat

  ============================

   nat_rect (fun n : nat => forall A : {set T}, n = #|A| -> nat)

     (fun (A' : {set T}) (_ : 0 = #|A'|) => 0)

     (fun (n : nat) (IHn : forall A : {set T}, n = #|A| -> nat) 

        (A : {set T}) (H : S n = #|A|) =>

      let (x, H0) := choosing' H in

      match H0 with

      | conj _ (conj H3 (conj _ _)) => IHn (A :\ x) H3 + g x

      end) #|set0| set0 eq_refl = 0

I can't make progress beyond this point because #|set0| seems inaccessible. (I want it to be 0 to simplify the nat_rect.) If I try

rewrite cards0. (*cards0

     : forall T : finType, #|set0| = 0*)

I get the error

Dependent type error in rewrite of (fun _pattern_value_ : nat =>

                                           nat_rect

                                             (fun n : nat =>

                                              forall A : {set T},

                                              n = #|A| -> nat)

                                             (fun (A' : {set T})

                                                (_ : 0 = #|A'|) => 0)

                                             (fun (n : nat)

                                                (IHn : 

                                                 forall A : {set T},

                                                 n = #|A| -> nat)

                                                (A : {set T})

                                                (H : S n = #|A|) =>

                                              let (x, H0) := choosing' H in

                                              match H0 with

                                              | conj _

                                                (conj H3 (conj _ _)) =>

                                                  IHn (A :\ x) H3 + g x

                                              end) _pattern_value_ set0

                                             eq_refl = 0)

and if I try to put cards0 as a hypothesis first:

pose (cards0 T) as H.

  intro g. unfold sums. unfold foldmap. rewrite -> H.

I get

Error: Abstracting over the term "#|set0|" leads to a term

"fun n : nat =>

 nat_rect (fun n0 : nat => forall A : {set T}, n0 = #|A| -> nat)

   (fun (A' : {set T}) (_ : 0 = #|A'|) => 0)

   (fun (n0 : nat) (IHn : forall A : {set T}, n0 = #|A| -> nat) 

      (A : {set T}) (H : S n0 = #|A|) =>

    let (x, H0) := choosing' H in

    match H0 with

    | conj _ (conj H3 (conj _ _)) => IHn (A :\ x) H3 + g x

    end) n set0 eq_refl = 0" which is ill-typed.

What gives?

Thanks,

Holden