I wrote this proof a while ago and I am not happy with the length and verbosity.

Does anyone have suggestions for how I can make it better / shorter?

I tried rewriting the code and came up with this which is not much better.

```
Proposition not_injective_hitstwice {n m : nat} (f : 'I_m^n) :
(injectiveb f) <-> (hitstwice f =1 xpred0).
Proof.
unfold injectiveb, dinjectiveb.
split. {
move => H a.
apply negbTE.
apply/negP => hits2x.
move : H.
apply/negP.
unfold hitstwice in hits2x.
move/existsP : hits2x => [x exy].
apply/(@uniqPn _ a).
move/existsP : exy => [y exprop].
exists x, y.
move/andP : exprop => [t1 fy_eq_a].
move/andP : t1 => [x_lt_y fx_eq_a].
rewrite x_lt_y.
rewrite size_map.
rewrite size_enum_ord.
rewrite (@nth_map _ x);
[ | case x as [xval xbd];
simpl; by rewrite size_enum_ord].
rewrite (@nth_map _ x _ a); [ | case x as [xval xbd]];
[ | case y as [yval ybd];
simpl; by rewrite size_enum_ord].
do 2 rewrite nth_ord_enum.
move/eqP : fx_eq_a => -> .
move/eqP : fy_eq_a => -> .
case y as [yval ybd]; simpl.
rewrite ybd.
done.
}
{
intros.
(* apply/card_uniqP. *)
(* Search card seq. *)
destruct m.
{ have -> :([seq f i | i <- _] = [::]).
{ move => ?.
apply empty_type_seq, card_ord.
}
done.
}
rewrite -[uniq _]negbK.
apply/negP.
rewrite -(rwP (uniqPn ord0)).
move => [i [j [i_lt_j j_lt_size]]].
rewrite size_map size_enum_ord in j_lt_size.
have j0 : 'I_n by exact (Sub j j_lt_size).
rewrite (nth_map j0 ord0 f); last first.
{ rewrite size_enum_ord; auto with arith. }
rewrite (nth_map j0 ord0 f); [ | now rewrite size_enum_ord ].
have i_lt_n : (i < n). { auto with arith. }
change i with (nat_of_ord (Sub i i_lt_n)).
rewrite nth_ord_enum.
change j with (nat_of_ord (Sub j j_lt_size)).
rewrite nth_ord_enum.
set ii := (Sub i i_lt_n).
set jj := (Sub j j_lt_size).
move => A.
have: hitstwice f (f ii).
{ rewrite /hitstwice.
apply/existsP. exists ii.
apply/existsP. exists jj.
simpl. rewrite i_lt_j eq_refl eq_sym /=.
now apply/eqP.
}
rewrite H.
done.
}
Qed.
```

Here is yet another attempt, it's a little better I think. I keep rewriting this looking for ideas for automation but I have not really stumbled across any aha moments that make me go "Oh, what if I wrote *this* in Ltac?"

This kind of proof I find very tedious and overly time consuming.

```
Proposition not_injective_hitstwice {n m : nat} (f : 'I_(m.+1)^n) :
(injectiveb f) <-> (hitstwice f =1 xpred0).
Proof.
split.
{
move => ib y.
rewrite (rwP (@negPf (hitstwice f y))) /hitstwice negb_exists.
apply/forallP => x0.
rewrite negb_exists.
apply/forallP => x1.
move/injectiveP : ib => ib.
destruct (@idP (f x0 == y)) as [eq0 | ]; [ | now rewrite andbF andFb].
destruct (@idP (f x1 == y)) as [eq1 | ]; [ | now rewrite andbF].
move/eqP : eq1.
move/eqP : eq0.
move => eq0 eq1.
have feq: f x0 = f x1 by congruence.
have xeq := ib _ _ feq.
now rewrite xeq ltnn.
}
{
move => h.
apply/injectiveP => x0 x1.
wlog: x0 x1 / (x0 <= x1 (* -> f x1 = f x2 -> x1 = x2 *)).
{
move => A t.
move: (leq_total x0 x1) => /orP [x0_le_x1 | x1_le_x0].
{ now apply A. }
{ symmetry; now apply:(A x1 x0). }
}
move => x0_leq_x1 feq.
apply/val_eqP.
rewrite (eqn_leq x0 x1).
rewrite x0_leq_x1 /= leqNgt.
set y := f x0; rewrite // in y.
have hy := h y.
rewrite /hitstwice in hy.
rewrite (rwP (negPf)) negb_exists in hy.
move/forallP: hy => hy.
have hyx0 := hy x0.
rewrite negb_exists in hyx0.
move/forallP: hyx0 => hyx0.
have hyx0x1 := hyx0 x1.
rewrite eq_refl in hyx0x1.
move/eqP : feq => feq.
rewrite eq_sym in feq.
rewrite feq in hyx0x1.
now do 2 rewrite andbT in hyx0x1.
}
Qed.
```

the most obvious comment I think is to always use `=`

instead of `<->`

whenever you can:

```
Proposition not_injective_hitstwice {n m : nat} (f : 'I_(m.+1)^n) :
(injectiveb f) = (hitstwice f =1 xpred0).
```

This is to me one of the big points of MathComp style specification, recovering the `<->`

for regular rewriting with `=`

as in HOL.

Here is a proof taking maximal advantage of boolean reflection:

```
Proposition not_injective_hitstwice {n m : nat} (f : 'I_(m.+1)^n) :
injectiveb f <-> hitstwice f =1 xpred0.
Proof.
split. {
move=> finj i; apply/existsPn => /= j; apply/existsPn => /= k.
case: ltnP => //= jk; apply/negP => /andP[/eqP <- /eqP/(injectiveP _ finj)].
by move=> /(congr1 val)/eqP; rewrite gtn_eqF//=. }
move=> ftwice; apply/injectiveP=> i j fifj.
wlog lt_ij : i j fifj / i < j => [hwlog|]. {
by have [/hwlog->|/hwlog->|/val_inj->] := ltngtP i j. }
have /existsPn/(_ i)/existsPn/(_ j) := ftwice (f i);
by rewrite lt_ij fifj eqxx.
Qed.
```

Note that there is not reason to use `injectiveb`

here rather than `injective`

and that shortens the proof (and potentially its usecases?)

```
Proposition not_injective_hitstwice {n m : nat} (f : 'I_(m.+1)^n) :
injective f <-> hitstwice f =1 xpred0.
Proof.
split. {
move=> finj i; apply/existsPn => /= j; apply/existsPn => /= k.
case: ltnP => //= jk; apply/negP => /andP[/eqP {i}<- /eqP /finj].
by move=> /(congr1 val)/eqP; rewrite gtn_eqF//=. }
move=> ftwice i j fifj; wlog lt_ij : i j fifj / i < j => [hwlog|]. {
by have [/hwlog->|/hwlog->|/val_inj->] := ltngtP i j. }
by have /existsPn/(_ i)/existsPn/(_ j) := ftwice (f i); rewrite lt_ij fifj eqxx.
Qed.
```

@Cyril Cohen Thanks, the use of injectiveb vs injective is more of a stylistic misunderstanding on my part of what the theorem statements are supposed to look like in SSReflect. My impression was that the goal is to state things using the boolean versions of things as much as possible and treat the propositional forms as like, specifications to be used to check the correctness of the boolean definitions

Last updated: Jul 23 2024 at 20:01 UTC