Skip to content
Snippets Groups Projects

Add `TCSimpl` type class.

Merged Add `TCSimpl` type class.
robbert/tcsimpl into master
1 unresolved thread
Merged Robbert Krebbers requested to merge robbert/tcsimpl into master
1 unresolved thread

See comment and test case for usage.

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Robbert Krebbers added 1 commit

    added 1 commit

    Compare with previous version

  • Robbert Krebbers added 1 commit

    added 1 commit

    Compare with previous version

  • Ralf Jung
  • Robbert Krebbers
    Robbert Krebbers @robbertkrebbers ·
    Author Owner

    Aside from the CHANGELOG, does this mean you are otherwise happy with this MR?

  • Ralf Jung
    Ralf Jung @jung ·
    Owner

    Yeah, generally speaking this makes sense. Do you have a concrete motivational usecase for this?

  • Robbert Krebbers
    Robbert Krebbers @robbertkrebbers ·
    Author Owner

    Yes, I have some lemmas that I want to iApply and automatically trigger simplification of subst. I do that by adding a TCSimpl premise.

  • Ralf Jung
    Ralf Jung @jung ·
    Owner

    Ah, that sounds fancy. Nice!

    Yeah LGTM.

  • Robbert Krebbers added 15 commits

    added 15 commits

    Compare with previous version

    Toggle commit list
  • Robbert Krebbers resolved all threads

    resolved all threads

  • Robbert Krebbers enabled an automatic merge when the pipeline for ab6bf9f9 succeeds

    enabled an automatic merge when the pipeline for ab6bf9f9 succeeds

  • Robbert Krebbers
    Robbert Krebbers @robbertkrebbers ·
    Author Owner

    Thanks, going to merge.

  • Robbert Krebbers merged

    merged

  • Robbert Krebbers mentioned in commit 47e0eddc

    mentioned in commit 47e0eddc

  • Janno
    Janno @janno started a thread on the diff
    • stdpp/base.v
    209 209 Lemma TCEq_eq {A} (x1 x2 : A) : TCEq x1 x2 ↔ x1 = x2.
    210 210 Proof. split; destruct 1; reflexivity. Qed.
    211 211
    212 (** The [TCSimpl x y] type class is similar to [TCEq] but performs [simpl]
    213 before proving the goal by reflexivity. Similar to [TCEq], the argument [x]
    214 is the input and [y] the output. When solving [TCEq x y], the argument [x]
    215 should be a concrete term and [y] an evar for the [simpl]ed result. *)
    216 Class TCSimpl {A} (x x' : A) := TCSimpl_TCEq : TCEq x x'.
    217 Global Hint Extern 0 (TCSimpl _ _) =>
    218 (* Since the second argument should be an evar, we can call [simpl] on the
    219 whole goal. *)
    220 simpl; notypeclasses refine (TCEq_refl _) : typeclass_instances.
    • Comment on lines +218 to +220
      Janno
      Janno @janno ·
      Maintainer

      simpl reduces in evar substitutions so calling simpl on the entire goal here can trigger nontrivial and unintended reduction. I would recommend binding the argument to be reduced and using let res := eval simpl in arg in .. instead.

      That being said, it's not clear to me when exactly evar substitutions would actually come about during TC search. AFAICT simpl does not perform reduction in the original evar context (which is an identity mapping of the coq context at the time the evar was created) so for fresh evars it might actually be fine to call simpl on the entire goal.

    • Robbert Krebbers
      Robbert Krebbers @robbertkrebbers ·
      Author Owner

      Can you make an issue for this, so that it's tracked?

      If you have a test case where the current instance fails, that would be even better.

    • Please register or sign in to reply
    Please register or sign in to reply