Shengyi Wang (Oct 28 2022 at 15:24): Shengyi Wang (Oct 28 2022 at 15:24):Now I defined a function about my trafficlight type. I want to prove some properties about \sum_. But I do not know how to enumerate my type.
Inductive trafficlight: predArgType := Red | Yellow | Green.
Definition trafficlight_eq (t1 t2: trafficlight): bool :=
match t1, t2 with
| Red, Red => true
| Yellow, Yellow => true
| Green, Green => true
| _, _ => false
end.
Definition traffic2ord (t: trafficlight): 'I_3 :=
match t with
| Red => inord O | Yellow => inord 1 | Green => inord 2
end.
Definition ord2traffic (o: 'I_3): option trafficlight :=
match val o with
| O => Some Red | 1 => Some Yellow | 2 => Some Green
| _ => None
end.
Lemma pcan_traffic_ord: pcancel traffic2ord ord2traffic.
Proof. by case; rewrite /ord2traffic /= inordK. Qed.
Lemma traffic_eqP : Equality.axiom trafficlight_eq. Proof. by do 2!case; constructor. Qed.
Canonical trafficlight_eqMixin := EqMixin traffic_eqP.
Canonical trafficlight_eqType := Eval hnf in EqType trafficlight trafficlight_eqMixin.
Definition trafficlight_choiceMixin := PcanChoiceMixin pcan_traffic_ord.
Canonical trafficlight_choiceType := ChoiceType trafficlight trafficlight_choiceMixin.
Definition trafficlight_countMixin := PcanCountMixin pcan_traffic_ord.
Canonical trafficlight_countType := CountType trafficlight trafficlight_countMixin.
Lemma trafficlight_enumP : Finite.axiom [:: Red; Yellow; Green]. Proof. by case. Qed.
Definition trafficlight_finMixin := FinMixin trafficlight_enumP.
Canonical trafficlight_finType := FinType trafficlight trafficlight_finMixin.
Lemma card_trafficlight: #| trafficlight | == 3. Proof. by rewrite cardT enumT unlock. Qed.
Definition light_val :=
fun x => match x with | Red => 1 | Yellow => 2 | Green => 3 end.
Lemma trafficlight_sum: \sum_(a in trafficlight) light_val a == 6.
I tried rewrite big_enum_val //=. and even rewrite BigOp.bigopE /reducebig /applybig /comp /index_enum unlock. to unfold everything. But Finite.enum is opaque. So I got stuck. Any suggestions? Thank you.
Ana de Almeida Borges (Oct 28 2022 at 19:28):There must be a better way, but after trying for awhile I grew annoyed and did what I tend to do when I'm annoyed: have an intermediate goal that seems simpler, even if I feel there must be a way to arrive there without spelling it out.
Lemma trafficlight_sum: \sum_(a in trafficlight) light_val a == 6.
Proof.
have -> : 6 = \sum_(i <- [:: Red; Yellow; Green]) light_val i.
by rewrite !big_cons big_nil.
apply/eqP; congr bigop => /=.
by rewrite /index_enum !unlock.
Qed.
By the way, since trafficlight is a finType, you can more simply write \sum_a light_val a.
Ana de Almeida Borges (Oct 28 2022 at 19:34):And I personally find it helpful to use _ = _ instead of _ == _ in lemma statements. You can always switch between them with eqP when you need the other, but usually when lemmas are equalities you want to use them to change the LHS into the RHS (or vice-versa), for which it is useful to have them in the _ = _ form.
Cyril Cohen (Oct 29 2022 at 16:02):@Ana de Almeida Borges's solution is really good, and it's bullet-proof since the summation does not depend on the order of the enumeration, which justifies unlocking.
Another way to phrase it is to state the canonical enumeration on the side, and use it.
Lemma enum_trafficlight : enum trafficlight = [:: Red; Yellow; Green].
Proof. by rewrite enumT unlock. Qed.
Lemma trafficlight_sum: \sum_a light_val a = 6.
Proof. by rewrite -big_enum enum_trafficlight !(big_cons, big_nil). Qed.
There is an alternative (more abstract) solution, which can be applied to decompose the proof into bits, in cases where the enumeration was not given explicitly and is hence known only up to a permutation:
Lemma enum_trafficlight : perm_eq (enum trafficlight) [:: Red; Yellow; Green].
Proof. by apply: (uniq_perm (enum_uniq _)) => // -[]; rewrite ?mem_enum. Qed.
Lemma trafficlight_sum: \sum_a light_val a = 6.
Proof.
by rewrite -big_enum (perm_big _ enum_trafficlight) !(big_cons, big_nil).
Qed.
Last updated: Apr 20 2024 at 10:02 UTC