Ssreflect Users Discussion List

[Cyril <>]

Thanks to you I found a shorter proof.
(I didn't know about big_load in the first place.)

Proof.
move=> Dop Did fop f1 I r P F; rewrite -big_all big_map big_filter => allD.
elim/(big_load (is_true \o mem D)): _; elim/big_ind3: _ allD => //=.
by move=> x y []// x' y' []// []// yD <- []// y'D <- _; rewrite fop ?Dop.
Qed.

In the end do we add this statement (or another one) to bigop?
What are your thoughts?

Best,
-- 
Cyril


On 24/11/2015 03:01, Emilio Jesús Gallego Arias wrote:
> Hello Cyril,
> 
> Cyril Cohen 
> <>
>  writes:
> 
>> What do you think of the following statement? And if you like it, do you
>> see minor/major shortcuts in the proof?
>>
>> Lemma big_morph_in (R1 R2 : Type)
>>   (f : R2 -> R1) (id1 : R1) (op1 : R1 -> R1 -> R1)
>>   (id2 : R2) (op2 : R2 -> R2 -> R2) (D : pred R2) :
>>   (forall x y, x \in D -> y \in D -> op2 x y \in D) ->
>>   id2 \in D ->
>>   {in D &, {morph f : x y / op2 x y >-> op1 x y}} ->
>>   f id2 = id1 ->
>>   forall  (I : Type) (r : seq I) (P : pred I) (F : I -> R2),
>>   all D [seq F x | x <- r & P x] ->
>>   f (\big[op2/id2]_(i <- r | P i) F i) =
>>   \big[op1/id1]_(i <- r | P i) f (F i).
>> Proof.
>> move=> Dop2 Did2 f_morph f_id I r P F.
>> elim: r => [|x r ihr /= DrP]; rewrite ?(big_nil, big_cons) //.
>> set b2 := \big[_/_]_(_ <- _ | _) _; set b1 := \big[_/_]_(_ <- _ | _) _.
>> have fb2 : f b2 = b1 by rewrite ihr; move: (P x) DrP => [/andP[]|].
>> case: (boolP (P x)) DrP => //= Px /andP[Dx allD].
>> rewrite f_morph ?fb2 // /b2 {b2 fb2 ihr b1 x Px Dx f_morph f_id}.
>> elim: r allD => [|x r ihr /=]; rewrite ?(big_nil, big_cons) //.
>> by case: (P x) => //= /andP [??]; rewrite Dop2 // ihr.
>> Qed.
> 
> Cool lemma, thanks for sharing it with us!
> 
> This is my attempt to do the proof; I'm not very happy with how line 3
> (and a bit line 2) is working here, maybe there is a better way to solve
> that part?
> 
> Proof.
> move=> Dop2 Did2 f_morph f_id I r P F.
> rewrite all_map; move/all_filterP; rewrite -filter_predI => hD.
> rewrite -big_filter -(@big_filter R1) -{1 2}hD !big_filter.
> elim/(big_load (is_true \o mem D)): _.
> elim/big_rec2: _ => //= i y1 y2 /andP [DFi Pi] [y2D fy2y1].
> by rewrite ?Dop2 ?f_morph ?fy2y1.
> Qed.
> 
> Best regards,
> Emilio
>