[demo] Add reification in src/Experiments/SimplyTypedArithmetic.v (#275)

* [demo] Add reification in src/Experiments/SimplyTypedArithmetic.v

It's rather verbose, unfortunately.  The reification also doesn't have
any of the nice debugging features of the version of reification in
Compilers, because that's even more boilerplate.  Not sure if I should
add that back in, at the moment.

Also, for some strange reason, places where `constr`s fail to typecheck
seem to induce backtracking where I don't think they should, and I'm not
sure what's going on...

* [demo] Add more namespacing

* Update llet notation, update is_known_const name

As per code review suggestions

* Namespace var_context, add some coqbug references

* Rename is_type_arg to is_template_parameter

As per https://github.com/mit-plv/fiat-crypto/pull/275#discussion_r153036059

* Simplify the logic around delayed arguments a bit

We no longer pass around dummy markers in the tuple of arguments.

* [demo] More informative reification error messages

This time without exponential slowdown in failure cases and without
needing to manually think up all of the possible errors and write them
out.

Possible thanks to Hugo's comment at
https://github.com/coq/coq/issues/6252#issuecomment-347041995

* [demo] respond to code review, add comments

* Update documentation with suggestions from Andres

1 files changed, 467 insertions, 10 deletions

diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v
index 5a839a842..94534b863 100644
--- a/src/Experiments/SimplyTypedArithmetic.v
+++ b/src/Experiments/SimplyTypedArithmetic.v
@@ -5,6 +5,8 @@ Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn.
 Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil.
 Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil.
 Require Import Crypto.Algebra.Ring Crypto.Util.Decidable.Bool2Prop.
+Require Import Crypto.Util.Tactics.RunTacticAsConstr.
+Require Import Crypto.Util.Notations.
 Import ListNotations. Local Open Scope Z_scope.
 
 Definition runtime_mul := Z.mul.
@@ -178,22 +180,470 @@ Module Positional. Section Positional.
   End mulmod.
 End Positional. End Positional.
 
-Import Associational Positional.
+Module Compilers.
+  Module type.
+    Inductive type := unit | prod (A B : type) | arrow (s d : type) | list (A : type) | nat | Z | bool.
+
+    Fixpoint interp (t : type)
+      := match t with
+         | unit => Datatypes.unit
+         | prod A B => interp A * interp B
+         | arrow A B => interp A -> interp B
+         | list A => Datatypes.list (interp A)
+         | nat => Datatypes.nat
+         | Z => BinInt.Z
+         | bool => Datatypes.bool
+         end%type.
+
+    Ltac reify ty :=
+      lazymatch eval cbv beta in ty with
+      | Datatypes.unit => unit
+      | Datatypes.prod ?A ?B
+        => let rA := reify A in
+           let rB := reify B in
+           constr:(prod rA rB)
+      | ?A -> ?B
+        => let rA := reify A in
+           let rB := reify B in
+           constr:(arrow rA rB)
+      | Datatypes.list ?T
+        => let rT := reify T in
+           constr:(list rT)
+      | Datatypes.nat => nat
+      | Datatypes.bool => bool
+      | BinInt.Z => Z
+      end.
+
+    Module Export Notations.
+      Delimit Scope ctype_scope with ctype.
+      Bind Scope ctype_scope with type.
+      Notation "()" := unit : ctype_scope.
+      Notation "A * B" := (prod A B) : ctype_scope.
+      Notation "A -> B" := (arrow A B) : ctype_scope.
+      Notation type := type.
+    End Notations.
+  End type.
+  Export type.Notations.
+
+  Module op.
+    Import type.
+    Inductive op : type -> type -> Set :=
+    | Const {t} (v : interp t) : op unit t
+    | Let_In {tx tC} : op (tx * (tx -> tC)) tC
+    | App {s d} : op ((s -> d) * s) d
+    | S : op nat nat
+    | nil {t} : op unit (list t)
+    | cons {t} : op (t * list t) (list t)
+    | fst {A B} : op (A * B) A
+    | snd {A B} : op (A * B) B
+    | bool_rect {T} : op (T * T * bool) T
+    | nat_rect {P} : op (P * (nat -> P -> P) * nat) P
+    | pred : op nat nat
+    | List_seq : op (nat * nat) (list nat)
+    | List_repeat {A} : op (A * nat) (list A)
+    | List_combine {A B} : op (list A * list B) (list (A * B))
+    | List_map {A B} : op ((A -> B) * list A) (list B)
+    | List_flat_map {A B} : op ((A -> list B) * list A) (list B)
+    | List_partition {A} : op ((A -> bool) * list A) (list A * list A)
+    | List_app {A} : op (list A * list A) (list A)
+    | List_fold_right {A B} : op ((B -> A -> A) * A * list B) A
+    | List_update_nth {T} : op (nat * (T -> T) * list T) (list T)
+    | Z_runtime_mul : op (Z * Z) Z
+    | Z_runtime_add : op (Z * Z) Z
+    | Z_add : op (Z * Z) Z
+    | Z_mul : op (Z * Z) Z
+    | Z_pow : op (Z * Z) Z
+    | Z_opp : op Z Z
+    | Z_div : op (Z * Z) Z
+    | Z_modulo : op (Z * Z) Z
+    | Z_eqb : op (Z * Z) bool
+    | Z_of_nat : op nat Z.
+
+    Notation curry2 f
+      := (fun '(a, b) => f a b).
+    Notation curry3 f
+      := (fun '(a, b, c) => f a b c).
+
+    Definition interp {s d} (opc : op s d) : type.interp s -> type.interp d
+      := match opc in op s d return type.interp s -> type.interp d with
+         | Const t v => fun _ => v
+         | Let_In tx tC => curry2 (@LetIn.Let_In (type.interp tx) (fun _ => type.interp tC))
+         | App s d
+           => fun '((f, x) : (type.interp s -> type.interp d) * type.interp s)
+              => f x
+         | S => Datatypes.S
+         | nil t => fun _ => @Datatypes.nil (type.interp t)
+         | cons t => curry2 (@Datatypes.cons (type.interp t))
+         | fst A B => @Datatypes.fst (type.interp A) (type.interp B)
+         | snd A B => @Datatypes.snd (type.interp A) (type.interp B)
+         | bool_rect T => curry3 (@Datatypes.bool_rect (fun _ => type.interp T))
+         | nat_rect P => curry3 (@Datatypes.nat_rect (fun _ => type.interp P))
+         | pred => Nat.pred
+         | List_seq => curry2 List.seq
+         | List_combine A B => curry2 (@List.combine (type.interp A) (type.interp B))
+         | List_map A B => curry2 (@List.map (type.interp A) (type.interp B))
+         | List_repeat A => curry2 (@List.repeat (type.interp A))
+         | List_flat_map A B => curry2 (@List.flat_map (type.interp A) (type.interp B))
+         | List_partition A => curry2 (@List.partition (type.interp A))
+         | List_app A => curry2 (@List.app (type.interp A))
+         | List_fold_right A B => curry3 (@List.fold_right (type.interp A) (type.interp B))
+         | List_update_nth T => curry3 (@update_nth (type.interp T))
+         | Z_runtime_mul => curry2 runtime_mul
+         | Z_runtime_add => curry2 runtime_add
+         | Z_add => curry2 Z.add
+         | Z_mul => curry2 Z.mul
+         | Z_pow => curry2 Z.pow
+         | Z_modulo => curry2 Z.modulo
+         | Z_opp => Z.opp
+         | Z_div => curry2 Z.div
+         | Z_eqb => curry2 Z.eqb
+         | Z_of_nat => Z.of_nat
+         end.
+
+    Module List.
+      Notation seq := List_seq.
+      Notation repeat := List_repeat.
+      Notation combine := List_combine.
+      Notation map := List_map.
+      Notation flat_map := List_flat_map.
+      Notation partition := List_partition.
+      Notation app := List_app.
+      Notation fold_right := List_fold_right.
+      Notation update_nth := List_update_nth.
+    End List.
+
+    Module Z.
+      Notation runtime_mul := Z_runtime_mul.
+      Notation runtime_add := Z_runtime_add.
+      Notation add := Z_add.
+      Notation mul := Z_mul.
+      Notation pow := Z_pow.
+      Notation opp := Z_opp.
+      Notation div := Z_div.
+      Notation modulo := Z_modulo.
+      Notation eqb := Z_eqb.
+      Notation of_nat := Z_of_nat.
+    End Z.
+
+    Module Export Notations.
+      Notation op := op.
+    End Notations.
+  End op.
+  Export op.Notations.
+
+  Inductive expr {var : type -> Type} : type -> Type :=
+  | TT : expr ()
+  | Pair {A B} (a : expr A) (b : expr B) : expr (A * B)
+  | Var {t} (v : var t) : expr t
+  | Op {s d} (opc : op s d) (args : expr s) : expr d
+  | Abs {s d} (f : var s -> expr d) : expr (s -> d).
+
+  Bind Scope expr_scope with expr.
+  Delimit Scope expr_scope with expr.
+  Notation "'λ'  x .. y , t" := (Abs (fun x => .. (Abs (fun y => t%expr)) ..)) : expr_scope.
+  Notation "( x , y , .. , z )" := (Pair .. (Pair x%expr y%expr) .. z%expr) : expr_scope.
+  Notation "( )" := TT : expr_scope.
+  Notation "()" := TT : expr_scope.
+  Notation "'expr_let' x := A 'in' b" := (Op op.Let_In (Pair A%expr (Abs (fun x => b%expr)))) : expr_scope.
+  Notation "f x" := (Op op.App (f, x)%expr) (only printing) : expr_scope.
+
+  Definition Expr t := forall var, @expr var t.
+
+  Fixpoint interp {t} (e : @expr type.interp t) : type.interp t
+    := match e with
+       | TT => tt
+       | Pair A B a b => (interp a, interp b)
+       | Var t v => v
+       | Op s d opc args => op.interp opc (interp args)
+       | Abs s d f => fun v => interp (f v)
+       end.
+
+  Definition Interp {t} (e : Expr t) := interp (e _).
+
+  Ltac is_known_const_cps2 term on_success on_failure :=
+    let recurse term := is_known_const_cps2 term on_success on_failure in
+    lazymatch term with
+    | S ?term => recurse term
+    | O => on_success ()
+    | Z0 => on_success ()
+    | Zpos ?p => recurse p
+    | Zneg ?p => recurse p
+    | xI ?p => recurse p
+    | xO ?p => recurse p
+    | xH => on_success ()
+    | ?term => on_failure term
+    end.
+  Ltac require_known_const term :=
+    is_known_const_cps2 term ltac:(fun _ => idtac) ltac:(fun term => fail 0 "Not a known const:" term).
+  Ltac is_known_const term :=
+    is_known_const_cps2 term ltac:(fun _ => true) ltac:(fun _ => false).
+
+  Definition Uncurry0 {A var} (opc : op type.unit A) : @expr var A
+    := Op opc TT.
+  Definition Uncurry1 {A B var} (opc : op A B) : @expr var (A -> B)
+    := λ a, Op opc (Var a).
+  Definition Uncurry2 {A B C var} (opc : op (A * B) C) : @expr var (A -> B -> C)
+    := λ a b, Op opc (Var a, Var b).
+  Definition Uncurry3 {A B C D var} (opc : op (A * B * C) D) : @expr var (A -> B -> C -> D)
+    := λ a b c, Op opc (Var a, Var b, Var c).
+
+  Ltac reify_op var term :=
+    (*let dummy := match goal with _ => idtac "attempting to reify_op" term end in*)
+    let Uncurry0 x := constr:(Uncurry0 (var:=var) x) in
+    let Uncurry1 x := constr:(Uncurry1 (var:=var) x) in
+    let Uncurry2 x := constr:(Uncurry2 (var:=var) x) in
+    let Uncurry3 x := constr:(Uncurry3 (var:=var) x) in
+    lazymatch term with
+    | S => Uncurry1 op.S
+    | @nil ?T
+      => let rT := type.reify T in
+         Uncurry0 (@op.nil rT)
+    | @cons ?T
+      => let rT := type.reify T in
+         Uncurry2 (@op.cons rT)
+    | seq => Uncurry2 op.List.seq
+    | @List.repeat ?A
+      => let rA := type.reify A in
+         Uncurry2 (@op.List.repeat rA)
+    | @Let_In ?A (fun _ => ?B)
+      => let rA := type.reify A in
+         let rB := type.reify B in
+         Uncurry2 (@op.Let_In rA rB)
+    | @combine ?A ?B
+      => let rA := type.reify A in
+         let rB := type.reify B in
+         Uncurry2 (@op.List.combine rA rB)
+    | @List.map ?A ?B
+      => let rA := type.reify A in
+         let rB := type.reify B in
+         Uncurry2 (@op.List.map rA rB)
+    | @List.flat_map ?A ?B
+      => let rA := type.reify A in
+         let rB := type.reify B in
+         Uncurry2 (@op.List.flat_map rA rB)
+    | @fst ?A ?B
+      => let rA := type.reify A in
+         let rB := type.reify B in
+         Uncurry1 (@op.fst rA rB)
+    | @snd ?A ?B
+      => let rA := type.reify A in
+         let rB := type.reify B in
+         Uncurry1 (@op.snd rA rB)
+    | @List.partition ?A
+      => let rA := type.reify A in
+         Uncurry2 (@op.List.partition rA)
+    | @List.app ?A
+      => let rA := type.reify A in
+         Uncurry2 (@op.List.app rA)
+    | @List.fold_right ?A ?B
+      => let rA := type.reify A in
+         let rB := type.reify B in
+         Uncurry3 (@op.List.fold_right rA rB)
+    | pred => Uncurry1 op.pred
+    | @update_nth ?T
+      => let rT := type.reify T in
+         Uncurry3 (@op.List.update_nth rT)
+    | runtime_mul => Uncurry2 op.Z.runtime_mul
+    | runtime_add => Uncurry2 op.Z.runtime_add
+    | Z.add => Uncurry2 op.Z.add
+    | Z.mul => Uncurry2 op.Z.mul
+    | Z.pow => Uncurry2 op.Z.pow
+    | Z.opp => Uncurry1 op.Z.opp
+    | Z.div => Uncurry2 op.Z.div
+    | Z.modulo => Uncurry2 op.Z.modulo
+    | Z.eqb => Uncurry2 op.Z.eqb
+    | Z.of_nat => Uncurry1 op.Z.of_nat
+    | @nat_rect (fun _ => ?T)
+      => let rT := type.reify T in
+         Uncurry3 (@op.nat_rect rT)
+    | @bool_rect (fun _ => ?T)
+      => let rT := type.reify T in
+         Uncurry3 (@op.bool_rect rT)
+    | _
+      => let assert_const := match goal with
+                             | _ => require_known_const term
+                             end in
+         let T := type of term in
+         let rT := type.reify T in
+         Uncurry0 (@op.Const rT term)
+    end.
+
+  Module var_context.
+    Inductive list {var : type -> Type} :=
+    | nil
+    | cons {t} (gallina_v : type.interp t) (v : var t) (ctx : list).
+  End var_context.
+
+  (* cf COQBUG(https://github.com/coq/coq/issues/5448) *)
+  Ltac refresh n :=
+    let n' := fresh n in
+    let n' := fresh n' in
+    let n' := fresh n' in
+    n'.
+
+  Ltac type_of_first_argument_of f :=
+    let f_ty := type of f in
+    lazymatch eval hnf in f_ty with
+    | forall x : ?T, _ => T
+    end.
+
+  (** Forms of abstraction in Gallina that our reflective language
+      cannot handle get handled by specializing the code "template" to
+      each particular application of that abstraction. In particular,
+      type arguments (nat, Z, (λ _, nat), etc) get substituted into
+      lambdas and treated as a integral part of primitive operations
+      (such as [@List.app T], [@list_rect (λ _, nat)]).  During
+      reification, we accumulate them in a right-associated tuple,
+      using [tt] as the "nil" base case.  When we hit a λ or an
+      identifier, we plug in the template parameters as necessary. *)
+  Ltac require_template_parameter parameter_type :=
+    first [ unify parameter_type Prop
+          | unify parameter_type Set
+          | unify parameter_type Type
+          | lazymatch eval hnf in parameter_type with
+            | forall x : ?T, @?P x
+              => let check := constr:(fun x : T
+                                      => ltac:(require_template_parameter (P x);
+                                               exact I)) in
+                 idtac
+            end ].
+  Ltac is_template_parameter parameter_type :=
+    is_success_run_tactic ltac:(fun _ => require_template_parameter parameter_type).
+  Ltac plug_template_ctx f template_ctx :=
+    lazymatch template_ctx with
+    | tt => f
+    | (?arg, ?template_ctx')
+      =>
+      let T := type_of_first_argument_of f in
+      let x_is_template_parameter := is_template_parameter T in
+      lazymatch x_is_template_parameter with
+      | true
+        => plug_template_ctx (f arg) template_ctx'
+      | false
+        => constr:(fun x : T
+                   => ltac:(let v := plug_template_ctx (f x) template_ctx in
+                            exact v))
+      end
+    end.
+
+  Ltac reify_helper var term value_ctx template_ctx :=
+    let reify_rec term := reify_helper var term value_ctx template_ctx in
+    (*let dummy := match goal with _ => idtac "reify_helper: attempting to reify:" term end in*)
+    lazymatch value_ctx with
+    | context[@var_context.cons _ ?rT term ?v _]
+      => constr:(@Var var rT v)
+    | _
+      =>
+      let term_is_known_const := is_known_const term in
+      lazymatch term_is_known_const with
+      | true => reify_op var term
+      | false
+        =>
+        lazymatch term with
+        | tt => TT
+        | @pair ?A ?B ?a ?b
+          => let ra := reify_rec a in
+             let rb := reify_rec b in
+             constr:(Pair (var:=var) ra rb)
+        | match ?b with true => ?t | false => ?f end
+          => let T := type of t in
+             reify_rec (@bool_rect (fun _ => T) t f b)
+        | let x := ?a in @?b x
+          => let A := type of a in
+             let B := lazymatch type of b with forall x, @?B x => B end in
+             reify_rec (@Let_In A B a b)
+        | ?f ?x
+          =>
+          let ty := type_of_first_argument_of f in
+          let x_is_template_parameter := is_template_parameter ty in
+          lazymatch x_is_template_parameter with
+          | true
+            => (* we can't reify things of type [Type], so we save it for later to plug in *)
+            reify_helper var f value_ctx (x, template_ctx)
+          | false
+            =>
+            let rx := reify_helper var x value_ctx tt in
+            let rf := reify_helper var f value_ctx template_ctx in
+            constr:(Op (var:=var) op.App (Pair (var:=var) rf rx))
+          end
+        | (fun x : ?T => ?f)
+          =>
+          let x_is_template_parameter := is_template_parameter T in
+          lazymatch x_is_template_parameter with
+          | true
+            =>
+            lazymatch template_ctx with
+            | (?arg, ?template_ctx)
+              => (* we pull a trick with [match] to plug in [arg] without running cbv β *)
+              reify_helper var (match arg with x => f end) value_ctx template_ctx
+            end
+          | false
+            =>
+            let rT := type.reify T in
+            let not_x := refresh x in
+            let not_x2 := refresh not_x in
+            let rf0 :=
+                constr:(
+                  fun (x : T) (not_x : var rT)
+                  => match f return _ with (* c.f. COQBUG(https://github.com/coq/coq/issues/6252#issuecomment-347041995) for [return _] *)
+                     | not_x2
+                       => ltac:(
+                            let f := (eval cbv delta [not_x2] in not_x2) in
+                            (*idtac "rec call" f "was" term;*)
+                            let rf := reify_helper var f (@var_context.cons var rT x not_x value_ctx) template_ctx in
+                            exact rf)
+                     end) in
+            lazymatch rf0 with
+            | (fun _ => ?rf)
+              => constr:(@Abs var rT _ rf)
+            | _
+              => (* This will happen if the reified term still
+              mentions the non-var variable.  By chance, [cbv delta]
+              strips type casts, which are only places that I can
+              think of where such dependency might remain.  However,
+              if this does come up, having a distinctive error message
+              is much more useful for debugging than the generic "no
+              matching clause" *)
+              let dummy := match goal with
+                           | _ => fail 1 "Failure to eliminate functional dependencies of" rf0
+                           end in
+              constr:(I : I)
+            end
+          end
+        | _
+          => let term := plug_template_ctx term template_ctx in
+             reify_op var term
+        end
+      end
+    end.
+  Ltac reify var term :=
+    reify_helper var term (@var_context.nil var) tt.
+  Ltac Reify term :=
+    constr:(fun var : type -> Type
+            => ltac:(let r := reify var term in
+                     exact r)).
+  Ltac Reify_rhs _ :=
+    let RHS := lazymatch goal with |- _ = ?RHS => RHS end in
+    let R := Reify RHS in
+    transitivity (Interp R);
+    [ | cbv beta iota delta [Interp interp op.interp Uncurry0 Uncurry1 Uncurry2 Uncurry3 Let_In type.interp bool_rect];
+        reflexivity ].
+End Compilers.
+Import Associational Positional Compilers.
 Local Coercion Z.of_nat : nat >-> Z.
 Local Coercion QArith_base.inject_Z : Z >-> Q.
-
 Definition w (i:nat) : Z := 2^Qceiling((25+1/2)*i).
-
-Example base_25_5_mul (f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 g0 g1 g2 g3 g4 g5 g6 g7 g8 g9 : Z)
+Example base_25_5_mul (*(f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 g0 g1 g2 g3 g4 g5 g6 g7 g8 g9 : Z)
         (f:=(f0 :: f1 :: f2 :: f3 :: f4 :: f5 :: f6 :: f7 :: f8 :: f9 :: nil)%list)
-        (g:=(f0 :: f1 :: f2 :: f3 :: f4 :: f5 :: f6 :: f7 :: f8 :: f9 :: nil)%list)
+        (g:=(f0 :: f1 :: f2 :: f3 :: f4 :: f5 :: f6 :: f7 :: f8 :: f9 :: nil)%list)*) (f g : list Z)
         (n:=10%nat)
+        (Hf : length f = n) (Hg : length g = n)
   : { fg : list Z | (eval w n fg) mod (2^255-19)
                     = (eval w n f * eval w n g) mod (2^255-19) }.
   (* manually assign names to limbs for pretty-printing *)
   eexists ?[fg].
   erewrite <-eval_mulmod with (s:=2^255) (c:=[(1,19)])
-      by (try eapply pow_ceil_mul_nat_nonzero; vm_decide).
+      by (try assumption; try eapply pow_ceil_mul_nat_nonzero; vm_decide).
 (*   eval w ?fg mod (2 ^ 255 - 19) = *)
 (*   eval w *)
 (*     (mulmod w (2^255) [(1, 19)] (f9,f8,f7,f6,f5,f4,f3,f2,f1,f0) *)
@@ -202,8 +652,14 @@ Example base_25_5_mul (f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 g0 g1 g2 g3 g4 g5 g6 g7 g8
 (*   ?fg = *)
 (*   mulmod w (2 ^ 255) [(1, 19)] (f9, f8, f7, f6, f5, f4, f3, f2, f1, f0) *)
 (*     (g9, g8, g7, g6, g5, g4, g3, g2, g1, g0) *)
-  cbv -[runtime_mul runtime_add]; cbv [runtime_mul runtime_add].
-  ring_simplify_subterms.
+  (*cbv [f g].*)
+  cbv [w Qceiling Qfloor Qopp Qnum Qdiv Qplus inject_Z Qmult Qinv Qden Pos.mul].
+  apply (f_equal (fun F => F f g)).
+  cbv [n].
+  cbv delta [mulmod w to_associational mul to_associational reduce from_associational add_to_nth zeros place split].
+  Reify_rhs ().
+  (*cbv -[runtime_mul runtime_add]; cbv [runtime_mul runtime_add].
+  ring_simplify_subterms.*)
 (* ?fg =
  (f0*g9+ f1*g8+    f2*g7+    f3*g6+    f4*g5+    f5*g4+    f6*g3+    f7*g2+    f8*g1+    f9*g0,
   f0*g8+ 2*f1*g7+  f2*g6+    2*f3*g5+  f4*g4+    2*f5*g3+  f6*g2+    2*f7*g1+  f8*g0+    38*f9*g9,
@@ -215,7 +671,8 @@ Example base_25_5_mul (f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 g0 g1 g2 g3 g4 g5 g6 g7 g8
   f0*g2+ 2*f1*g1+  f2*g0+    38*f3*g9+ 19*f4*g8+ 38*f5*g7+ 19*f6*g6+ 38*f7*g5+ 19*f8*g4+ 38*f9*g3,
   f0*g1+ f1*g0+    19*f2*g9+ 19*f3*g8+ 19*f4*g7+ 19*f5*g6+ 19*f6*g5+ 19*f7*g4+ 19*f8*g3+ 19*f9*g2,
   f0*g0+ 38*f1*g9+ 19*f2*g8+ 38*f3*g7+ 19*f4*g6+ 38*f5*g5+ 19*f6*g4+ 38*f7*g3+ 19*f8*g2+ 38*f9*g1) *)
-  trivial.
-Defined.
+  (*trivial.
+Defined.*)
+Abort.
 
 (* Eval cbv on this one would produce an ugly term due to the use of [destruct] *)