discrinimationtrees.v

From Coq Require Import Lia.

Axiom P : nat -> Prop.

Module wasteful_search.

  Class Simplify (n : nat) :=
    { simplified_to : nat; simplified_ok : P n -> P simplified_to }.


  Program Instance SimplifyAddAssoc {x y z} : Simplify ((x + (y + z))) | 0 :=
    {| simplified_to := (x+y+z) |}.
  Next Obligation. rewrite Plus.plus_assoc_reverse. assumption. Qed.

  Program Instance SimplifyAdd0 {x} : Simplify ((x + 0)) | 0 :=
    {| simplified_to := (x) |}.
  Next Obligation. rewrite plus_n_O. assumption. Qed.

  Program Instance SimplifyAdd0' {x} : Simplify (x + 1) | 0 :=
    {| simplified_to := (1 + x) |}.
  Next Obligation. rewrite PeanoNat.Nat.add_1_r in H. assumption. Qed.

  Program Instance SimplifyMulAssocL {x y z} : Simplify ((x * (y * z) )) | 1 :=
    {| simplified_to := (x*y*z) |}.
  Next Obligation. rewrite Mult.mult_assoc_reverse. assumption. Qed.


  Goal forall x y z, P (x * (y * z)) -> True.
    intros x y z H.
    Set Typeclasses Debug.
    Set Typeclasses Debug Verbosity 100.
    apply (@simplified_ok _ _) in H.
    (* Tries to apply all instances for addition. *)
  Abort.
End wasteful_search.


Module smarter_search.
  Class Simplify (n : nat) :=
  { simplified_to : nat; simplified_ok : P n -> P simplified_to }.

  (* Stratify classes to help the search algorithm *)

  Class SimplifyAdd (n1 n2 : nat) :=
    { simplified_add :> Simplify (n1 + n2) }.

  Program Instance SimplifyAddAssoc {x y z} : SimplifyAdd x (y + z) | 0 :=
    {| simplified_add := {| simplified_to := (x + y + z) |} |}.
  Next Obligation. rewrite Plus.plus_assoc_reverse. assumption. Qed.

  Program Instance SimplifyAdd0 {x} : SimplifyAdd x  0 | 0 :=
    {| simplified_add := {| simplified_to := x |} |}.
  Next Obligation. rewrite plus_n_O. assumption. Qed.

  Program Instance SimplifyAdd0' {x} : SimplifyAdd x 1 | 0 :=
    {| simplified_add := {| simplified_to := 1 + x |} |}.
  Next Obligation. rewrite PeanoNat.Nat.add_1_r in H. assumption. Qed.

  Program Instance SimplifyMulAssocL {x y z} : Simplify ((x * (y * z) )) | 1 :=
    {| simplified_to := (x*y*z) |}.
  Next Obligation. rewrite Mult.mult_assoc_reverse. assumption. Qed.


Goal forall x y z, P (x * (y * z)) -> True.
  intros x y z H.
  Set Typeclasses Debug.
  Set Typeclasses Debug Verbosity 100.
  apply (@simplified_ok _ _) in H.
  (* doesn't even try SimplifyAdd at all and even if it did it would fail immediately without trying all the instances of SimplifyAdd *)
Abort.
End smarter_search.