Demo.v

Module MatchContext.
  Inductive D :=
  | d_a : D
  | d_b : D -> D -> D.
  Fixpoint cmpl d := match d with
                     | d_a => 1
                     | d_b x x0 => S (cmpl x + cmpl x0)
                     end.
  Record T d := {a : d; b : d}.
  Import ListNotations.
  Require Import Omega.
  Local Obligation Tactic := Tactics.program_simpl; autounfold; try solve [simpl; omega]; try solve [repeat split; congruence].  
  Program Fixpoint rule_transform (ed : T D) {measure (cmpl (a _ ed) + cmpl (b _ ed))} : (list (T D)) :=
    let av := a _ ed in
    let bv := b _ ed in
    match (av, bv) return list (T D) with
    | (d_b a1 a2, d_b b1 b2) =>
      rule_transform {|a:=a1;b:=b1|} (* even here it generates an obligation where the relation of the sides is lost despite there not being any higher order functions involved that need to be unfolded *)
    | (a, b) => ([ed])
    end.
  Next Obligation. Abort. (* Unprovable because context is missing*)
  Admit Obligations. 

 

  Program Fixpoint rule_transform' (ed : T D) {measure (cmpl (a _ ed) + cmpl (b _ ed))} : (list (T D)) :=
    let av := a _ ed in
    let bv := b _ ed in
    match (av, bv) with
    | (d_b a1 a2, d_b b1 b2) =>
      rule_transform' {|a:=a1;b:=b1|} (* Here we get the context although the statement itself hasn't changed *)
    | (a, b) => ([ed])
    end.
(* works *)
End MatchContext.