Giving access in `match` to the expansion of the term being matched via an alias in order to support more fixpoints

[herbelin]

Rendered here.

[herbelin]

@SkySkimmer: Nice! Your "commutative cut" indeed provides a simple encoding of match with the extra as, which works also for the guard thanks to the propagation of the size through commutative cuts.

For the record, I add the working parametricity of (a simplification of) gcd which relies on sub:

Fixpoint G (a b : nat) {struct a} : nat :=
  match a return nat with
  | O => b
  | S a' => G (Nat.sub a' b) (S a')
  end.

Fixpoint is_G a (is_a : is_nat a) b (is_b : is_nat b) {struct is_a} : is_nat (G a b) :=
  match is_a in is_nat a return is_nat (G a b) with
  | is_O => is_b
  | is_S a' P_ => is_G _ (is_sub a' P_ b is_b) (S a') (is_S a' P_)
    (* failed with the variant of is_sub w/o generalization that returns the expansion of Pn *)
  end.

[herbelin]

I guess this new justification still leads to two possible points of view:

• it is useless because emulatable,
• it is emulatable so it is "safe" to conveniently provide this "direct" style.