The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2015-05-13 14:07 GMT+02:00 Holden Lee <holdenlee AT alum.mit.edu>:

Thanks, I will use bigop.

Still, I'd like to understand the error. How would I "generalize" over eq_refl? Here eq_refl should be of type #|set0|=#|set0|. How can I tell Coq that the type 0=#|set0| is the same as #|set0|=#|set0|, if not using rewrite?

Thanks,

Holden

​I will try to clarify your situation:

You want to prove "P #|set0| set0 eq_refl = 0" where P has type: ∀ n A, n = #|A| → nat.

If you want to rewrite #|set0| as 0, then that means that you want to get something like "P 0 set0 H = 0" where H has type "0=#|set0|".

Well, "eq_refl" has type (after instantiating implicits) either 0=0 or #|set0|=#|set0|, but neither of them have the same type as H.

So now, if you consider the following definition "X := fun n => ∀ (H:n=#|set0|), (P n set0 H = 0)", then X is well typed (of type: nat→Prop).
If you can prove "X 0" which proof term would be "π" (ie. "π" has type "X 0"), then you are done.
"ρ := match cards0 in _=c return X 0 -> X c with eq_refl => fun z=>z end" has type "X 0 → X #|set0|".
Thus "ρ π eq_refl" has type "P #|set0| set0 eq_refl = 0" which is precisely what you want.

Unless I am wrong, "π := fun (H:0=#|set0|) => (((eq_refl 0) : 0 = 0) : P 0 set0 H = 0)" should work.

This is a way to "generalize over eq_refl" in a rather manual way (you directly write proof terms).

I think it is good to do that manually at least once to have better understandings of what happens.

Once you will be used to this logic, either you will design your goals "smartly" so that this way to do will not be too cumbersome, either you will use black magic of tactics (well in fact not so black once you have understood the mechanics behind…).

So with no intermediate definitions and more tactic stuff, you get:

>generalize eq_refl.

Which turns your goal into

forall (H:#|set0|=#|set0|), P #|set0| set0 H = 0

From there, you can generalize again (well, maybe that the pattern tactic can be useful here as well)

>generalize #|set0| at 1 3. (* Not sure of the occurences, I have no running coq for now, but you get the idea *)

This turns your goal as:

forall n (H:n=#|set0|), P n set0 H = 0

From there get "n" and its specification:

>intros n Hn.

Duplicate Hn, and revert it:

>generalize Hn.

You get:

forall (H:n=#|set0|), P n set0 H = 0

and have "Hn : n=#|set0|" in your context, thus thanks to "card0", you can rewrite n as 0.

>rewrite card0 in Hn; rewrite Hn.

You get:

forall (H: 0=#|set0|), P 0 set0 H = 0

​From here, you can simplify,

>simpl.

and get something like:

0=#|set0| → 0 = 0

which should not be too hard to prove.

I am not a powerful tactic user, so there may be tactics which do all that in less steps or in less annoying way (I mainly think of determining the occurrences in the "generalize … at …." tactic).

 

On Wed, May 13, 2015 at 5:27 AM, Pierre-Yves Strub <pierre-yves AT strub.nu> wrote:

Also, I don't know how you defined foldmap, but I bet that you're folding on the size of the set, picking one element at each iteration.

As a general remark, folding over the (list) enumeration of the set (or over the enumeration of the finType, filtering by membership) seems much more practical.

2015-05-13 11:22 GMT+02:00 Pierre-Yves Strub <pierre-yves AT strub.nu>:

Hi,

Why not using bigops ? For instance, you have:

big_set0

     : forall (R : Type) (idx : R) (op : law idx) (I : finType) (F : I -> R),

       \big[op/idx]_(i in set0) F i = idx

Best,

-- Pierre-Yves.

2015-05-13 4:24 GMT+02:00 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