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

[herbelin]

Rendered here.

[SkySkimmer]

Maybe we should be using some sort of convoy pattern?

Fixpoint sub (n m : nat) {struct n} : nat :=
  match n with
  | 0 => fun n => n
  | S k => fun n =>
      match m with
      | 0 => n
      | S l => sub k l
      end
  end n.

Inductive is_nat : nat -> Prop :=
| is_O : is_nat 0
| is_S x : is_nat x -> is_nat (S x).

Fixpoint is_sub (n : nat) (Pn : is_nat n) (m : nat) (Pm : is_nat m) : is_nat (Nat.sub n m) :=
  match Pn in (is_nat n) return is_nat n -> is_nat (Nat.sub n m) with
  | is_O => fun p => p
  | is_S x P_ => fun p =>
      match
        Pm in (is_nat m0)
        return is_nat (match m0 with 0 => S x | S l => Nat.sub x l end)
      with
      | is_O => p
      | is_S l Pl => is_sub x P_ l Pl
      end
  end Pn.

works (not sure if that's exactly what parametricity would produce)

[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.