Generate simplification lemmas

[MarvinLira]

Description

For each function that is translated there should be some lemmas generated from the IR that can be used in combination with a hint database and autorewrite to replace the Coq tactics simpl and unfold. Those lemmas should in some way skip the initial pattern matchings.

append :: [a] -> [a] -> [a]
append xs ys = case xs of
  [] -> ys
  x : xs -> case xs of
    [] -> x : xs
    (x' : xs') -> x : x' : (append xs' ys)

(* Simplification lemmas for append. *)

(* Impure case for first case destruction. *)
Lemma simpl_append1 :
  forall (Shape : Type) (Pos : Shape -> Type)
           (a : Type)
           (s : Shape) (pf : Pos s -> Free Shape Pos (List Shape Pos a))
           (ys : Free Shape Pos (List Shape Pos a)),
    append Shape Pos (impure s pf) ys = impure s (fun p -> append Shape Pos (pf p) ys).
Proof. trivial. Qed.

(* First case of first case destruction. *)
Lemma simpl_append2 :
  forall ...,
    append Shape Pos (Nil Shape Pos) ys = ys
Proof. trivial. Qed.

(* Impure case for second case destruction in second case of first case destruction. *)
Lemma simpl_append3 :
  forall ...,
    append Shape Pos (Cons x Shape Pos (impure s pf)) ys
    = impure s (append Shape Pos (Cons x Shape Pos (pf p)) ys).
Proof. trivial. Qed.

(* First case of second case destruction in second case of first case destruction. *)
Lemma simpl_append4 :
  forall ...,
    append Shape Pos (Cons x Shape Pos (Nil Shape Pos)) ys = Cons Shape Pos x ys.
Proof. trivial. Qed.

(* Second case of second case destruction in second case of first case destruction. *)
Lemma simpl_append5 :
  forall ...,
    append Shape Pos (Cons x Shape Pos (Cons Shape Pos x' xs')) ys
    = Cons Shape Pos x (Cons Shape Pos x' (append Shape Pos Shape Pos xs' ys)).
Proof. trivial. Qed.

(* Add simplification lemmas to a hint database. *)
Hint Rewrite simpl_append1 : simplDB.
...
Hint Rewrite simpl_append5 : simplDB.

The database simpleDB should be a hint database that is used for every simplification lemma of every modul. According to this, the database does not have to be declared before adding hints, but it should be declared in some central place for documentation reasons.
There are some things to note here:

• Recursive calls of the function do not use some helper functions generated by the compiler but the original function.
• For each case destruction there is an implicit case where the value which gets destructed is impure.

Motivation

The Coq tactics simpl an unfold have some disadvantages in our use case. They simplificate too much and expose things like helper functions, that are defined for recursive functions, and bind operators. Those things should be hidden from the user as far as possible and might make it harder to proceed with a proof. If using autorewrite with simplDB instead those helper functions are hidden and the number of bind operators is reduced.

Alternatives

Those generic names simpl_append1 etc. could be replaced by a name that gives a hint on the pattern matching it represents.

Additional Context

A guard g of a pattern matching could be translated as a precondition g = pure true ->. The following cases had to use the additional precondition g = pure false -> to ensure correctness. This would however also generate a new impure case for g = impure s pf. To keep things simple we should start with unguarded cases.