Library ASCommon.CDestruct


From Stdlib Require Import Program.Equality.
From stdpp Require Import sets.

Require Import Options.
Require Import CBase.
Require Export CSimp.

CDestruct is context cleaner/clarifier.
It will process a set of hypotheses (both in the context and goal), as well as possibly the goal. The current syntax is:
  • cdestruct h,h2: processes h and h2 and any context hypotheses that depend on them (i.e. generalize dependent)
  • cdestruct |- ??: Processes the first 2 hypotheses in the goal A → B → G
  • cdestruct |- **: Processes all the hypotheses in the goal, but not the goal For example if goal is A → G (and G is not a product), then this processes only A
  • cdestruct |- ***: Processes all the hypotheses in the goal and the goal itself.
  • Combinations like cdestruct h,h2 |- ** also work.
  • cdestruct ... as intro_pattern can be used to name the generated hypotheses. If less names than needed are provided, the corresponding hypotheses are left in the goal. cdestruct ... as will leave everything in the goal.
The goal of cdestruct is to perform a set of user-specified simplification/clarification rules without backtracking to bring the goal in a cleaner state, or discharge the goal if it is trivial after those simplifications.
cdestruct should not introduce evars and tries to not fill any either. However it is relatively easy to add hints that would do either and there is currently no check for that, but it could break the safeness properties
On each specified hypotheses, cdestruct will perform the following:
  • Split all types specified by CDestrCase. By default:
    • pairs, ∧, ∃, False, True
    • If CDestrSplitGoal is specified: ∨, +, ...
  • Simplify with cbn (Always on, can't be disabled for now)
  • discharge if an hypothesis is trivially false:
    • discriminate and contradiction
    • x ≠ x
  • Clean up t = t
  • Apply all rewritings in CDestrSimpl false, by default:
    • Simplifying obviously false as defined ObvFalse into False, by default:
      • contradicting hypotheses (contradiction)
      • different constructor equalities (discriminate)
      • x ≠ x
    • Injectivity of constructors (with less that 4 different parameters)
    • Injectivity of record constructor when enabled with CDestrRecInj
    • Boolean tautologies: ¬¬P to P, and some De Morgan laws
    • equalities with bool_decide
    • Simplifying ctrans calls when possible.
  • If an hypothesis implies an equality that is substituable, (as defined by CDestrSubst), then do the substitution. By default:
    • A plain variable equality x = expr or expr = y
    • existsT T x = existsT T' x' if either T or T' is a variable
    • The same with constructor nesting: existsT (existT T x) y = existT (existT T' x') y'), if either T or T' is a variable. - Also by default with other constructors than [existT] - [ctrans e f] anywhere if [e] has a variable on either side - If a there is a match of a type (or [inspect] of a type), and the type is in [CDestrMatchT], then destruct the discriminee (and keep the equality if not a variable) Then on the goal [cdestruct] will perform the following: - Split all types specified by [CDestrSplit]. By default: - [True] - If [CDestrSplitGoal] is specified: [∧], [↔]. ... - Discharge if the goal is obviously true ([ObvTrue]). By default: - [reflexivity], [assumption], [eassumption]. - Perform all rewriting given by [CDestrSimpl true] it's possible to have different rewriting than in an hypothesis context - Try [CDestrGoalSuperSubst] substitution that come from the goal's type, mostly things like try substitution on [e] when [ctrans e f] is in the goal. - Break match cases in the same way as in the hypotheses. In addition we have a few immediate improvement plans: - Do not reintroduce the same hypothesis twice - This would allow to have some basic system of fact saturation - Potentially the substitution system could be replaced by saturating with the extracted equality - Need to think how to do saturation from the goal without doing the same things multiple times (e.g. extract [e] from a goal containing [ctrans e f]) Longer term we probably also need to improve the simplification system for performance, and make typeclass resolution faster/simpler in general.

Injectivity

This is a is done with a bunch of injectivity typeclasses, that can be used elsewhere. This enforce that any injection done by cdestruct respects typeclass opaqueness (unlike the regular injection)
Deduce Inj instance from dependent injection.
#[export] Hint Extern 20 (Inj ?A eq ?Constr) ⇒
  eunify A eq;
  unfold Inj;
  by simplify_dep_elim
  : typeclass_instances.

Create HintDb inj discriminated.

Use f_equal automatically and safely on injective functions
Hint Extern 1 (?f ?x = ?f ?y) ⇒
       has_option (Inj (=) (=) f);
       simple apply (f_equal f) : inj.

Deduce Inj2 instance from dependent injection. This might use UIP
#[export] Hint Extern 20 (Inj2 ?A ?B eq ?Constr) ⇒
  eunify A eq;
  eunify B eq;
  unfold Inj2;
  by simplify_dep_elim
  : typeclass_instances.

Lemma inj2_iff `{Inj2 A B C RA RB RC f} {HP : Proper (RA ==> RB ==> RC) f}
  x1 x2 y1 y2 :
  RC (f x1 x2) (f y1 y2) ↔ RA x1 y1 ∧ RB x2 y2.
Proof. split; intro; [by apply (inj2 f) | apply HP; naive_solver]. Qed.
Arguments inj2_iff {_ _ _ _ _ _} _ {_ _}.

Use f_equal automatically and safely on injective functions
Hint Extern 1 (?f _ _ = ?f _ _) ⇒
       has_option (Inj2 (=) (=) (=) f);
       simple apply (f_equal2 f) : inj.

Class Inj3 {A B C D} (R1 : relation A) (R2 : relation B) (R3 : relation C)
    (S : relation D) (f : A → B → C → D) : Prop := inj3 x1 x2 x3 y1 y2 y3 :
    S (f x1 x2 x3) (f y1 y2 y3) → R1 x1 y1 ∧ R2 x2 y2 ∧ R3 x3 y3.
Global Arguments inj3 {_ _ _ _ _ _ _ _} _ {_} _ _ _ _ _ _ _: assert.

Lemma inj3_iff `{Inj3 A B C D R1 R2 R3 RS f}
  {HP : Proper (R1 ==> R2 ==> R3 ==> RS) f} x1 x2 x3 y1 y2 y3 :
  RS (f x1 x2 x3) (f y1 y2 y3) ↔ R1 x1 y1 ∧ R2 x2 y2 ∧ R3 x3 y3.
Proof. split; intro; [by apply (inj3 f) | apply HP; naive_solver]. Qed.
Arguments inj3_iff {_ _ _ _ _ _ _ _} _ {_ _}.

Deduce Inj3 instance from dependent injection. This might use UIP
#[export] Hint Extern 20 (Inj3 ?A ?B ?C eq ?Constr) ⇒
  eunify A eq;
  eunify B eq;
  eunify C eq;
  unfold Inj3;
  by simplify_dep_elim
  : typeclass_instances.

Use f_equal automatically and safely on injective functions
Hint Extern 1 (?f _ _ _ = ?f _ _ _) ⇒
       has_option (Inj3 (=) (=) (=) (=) f);
       simple apply (f_equal3 f) : inj.

Class Inj4 {A B C D E} (R1 : relation A) (R2 : relation B) (R3 : relation C)
  (R4 : relation D) (S : relation E) (f : A → B → C → D → E) : Prop :=
  inj4 x1 x2 x3 x4 y1 y2 y3 y4 :
    S (f x1 x2 x3 x4) (f y1 y2 y3 y4) →
    R1 x1 y1 ∧ R2 x2 y2 ∧ R3 x3 y3 ∧ R4 x4 y4.
Global Arguments inj4 {_ _ _ _ _ _ _ _ _ _} _ {_} _ _ _ _ _ _ _ _ _: assert.

Lemma inj4_iff `{Inj4 A B C D E R1 R2 R3 R4 RS f}
  {HP : Proper (R1 ==> R2 ==> R3 ==> R4 ==> RS) f} x1 x2 x3 x4 y1 y2 y3 y4 :
  RS (f x1 x2 x3 x4) (f y1 y2 y3 y4) ↔ R1 x1 y1 ∧ R2 x2 y2 ∧ R3 x3 y3 ∧ R4 x4 y4.
Proof. split; intro; [by apply (inj4 f) | apply HP; naive_solver]. Qed.
Arguments inj4_iff {_ _ _ _ _ _ _ _ _ _} _ {_ _}.

#[export] Hint Rewrite @inj_iff using tc_solve : inj.
#[export] Hint Rewrite @inj2_iff using tc_solve : inj.
#[export] Hint Rewrite @inj3_iff using tc_solve : inj.
#[export] Hint Rewrite @inj4_iff using tc_solve : inj.

Deduce Inj4 instance from dependent injection. This might use UIP
#[export] Hint Extern 20 (Inj4 ?A ?B ?C ?D eq ?Constr) ⇒
  eunify A eq;
  eunify B eq;
  eunify C eq;
  eunify D eq;
  unfold Inj4;
  by simplify_dep_elim
  : typeclass_instances.

Use f_equal automatically and safely on injective functions
Hint Extern 1 (?f _ _ _ _ = ?f _ _ _ _) ⇒
       has_option (Inj4 (=) (=) (=) (=) (=) f);
       simple apply (f_equal4 f) : inj.

ObvFalse

This typeclass gathers facts that are obviously false. If you have a theory specific way of deriving false, you can add it to this typeclass. cdestruct will then use this to simplify those fact into False (and discharge the goal if those are in the context)
#[local] Set Typeclasses Strict Resolution.
Class ObvFalse (P : Prop) := {obv_false : P → False}.
#[local] Unset Typeclasses Strict Resolution.

Global Instance obv_false_False : ObvFalse False.
Proof. by tcclean. Qed.

Global Instance obv_false_neq A (x : A) : ObvFalse (x ≠ x).
Proof. by tcclean. Qed.

Global Hint Extern 8 (ObvFalse _) ⇒
  let H := fresh "H" in
  constructor; intro H; (contradiction H || discriminate H) : typeclass_instances.

Incompatible

This typeclass flags mutually exclusive properties of an object, like discriminate but for non inductives. If there are n incompatible statements this setup still requires n(n-1)/2 Instances. TODO improve that
Class Incompatible (P : Prop) (Q : Prop) := {incompatible : P → Q → False}.
#[global] Hint Mode Incompatible + - : typeclass_instances.
#[global] Hint Mode Incompatible - + : typeclass_instances.

#[global] Instance obv_false_incompatible_l `{Incompatible P Q} :
  TCFastDone P → ObvFalse Q.
Proof. deintro. tcclean. naive_solver. Qed.

#[global] Instance obv_false_incompatible_r `{Incompatible P Q} :
  TCFastDone Q → ObvFalse P.
Proof. deintro. tcclean. naive_solver. Qed.

ObvTrue

This typeclass gathers fact that are obviously true, this allows to solve the goal quickly if possible, try to limit the search time though. fast_done is and example of what it expected to be solved by this typeclass.

#[local] Set Typeclasses Strict Resolution.
Class ObvTrue (P : Prop) := {obv_true : P}.
#[local] Unset Typeclasses Strict Resolution.

Instance obv_true_True : ObvTrue True.
Proof. now tcclean. Qed.

Instance obv_true_not_False : ObvTrue (¬ False).
Proof. now tcclean. Qed.

This will only do reflexivity up to typeclass transparency
Instance obv_true_eq_refl {A} (x : A) : ObvTrue (x = x).
Proof. now tcclean. Qed.

Global Hint Extern 3 (ObvTrue _) ⇒
         constructor; assumption : typeclass_instances.

Global Hint Extern 4 (ObvTrue _) ⇒
         constructor; symmetry; assumption : typeclass_instances.

Global Hint Extern 2 (ObvTrue ?p) ⇒
         assert_fails (has_evar p);
         constructor; solve [constructor] : typeclass_instances.

Instance obvTrue_or_left P Q : ObvTrue P → ObvTrue (P ∨ Q).
Proof. tcclean. naive_solver. Qed.

Instance obvTrue_or_right P Q : ObvTrue Q → ObvTrue (P ∨ Q).
Proof. tcclean. naive_solver. Qed.

CDestruct

See the top of the file comment for details about what cdestruct does.

CDestruct options

If CDestrCase is enabled for a type, then cdestruct will destruct that type when it sees it in an hypothesis
#[local] Set Typeclasses Strict Resolution.
Class CDestrCase (T : Type) := {}.
#[local] Unset Typeclasses Strict Resolution.

If CDestrSplit is enabled for a type, then cdestruct will split that type when it sees it in the goal
#[local] Set Typeclasses Strict Resolution.
Class CDestrSplit (T : Type) := {}.
#[local] Unset Typeclasses Strict Resolution.

cdestruct will apply all simplification provided by CDestrSimpl If is provided by CDestrSimpl false it will be an hypothesis simplification, otherwise it will be a goal simplification.
Class CDestrSimpl (goal : bool) (P Q : Prop) := cdestr_simpl {cdestruct_simpl : P ↔ Q}.
Global Hint Mode CDestrSimpl + ! - : typeclass_instances.
Arguments cdestr_simpl _ {_ _} _.
Arguments cdestruct_simpl _ _ {_ _}.
Useful for blocked_evar resolution in block_all_evars
Ltac get_cdestr_simpl_evars _ :=
  lazymatch goal with
  | |- CDestrSimpl _ ?G _ ⇒ G
  end.

CDestrSubst try to extract a variable substitution from a given proposition P that cannot be directly simplified. CDestrSimpl is tried before CDestrSubst. The output proposition Q must have the form x = expr or expr = y where x or y respectively is a variable. Otherwise the instance found is rejected (and cdestruct wastes time).
One simple case is if P itself is x = expr with x a variable. However more subtle cases are possible such as P = (existT x expr1 = existT expr2 expr3)
There is a Hint Extern below that tries to find the simple case of that pattern generically
Class CDestrSubst (P : Prop) (Q : Prop) :=
  cdestr_subst {cdestruct_subst : P → Q}.
Global Hint Mode CDestrSubst ! - : typeclass_instances.
Arguments cdestr_subst {_ _} _.
Arguments cdestruct_subst _ {_ _}.
Ltac get_cdestr_subst_evars _ :=
  lazymatch goal with
  | |- CDestrSubst ?G _ ⇒ G
  end.

This is the goal version of the previous to extract equalities from the goal that could be used for substitution, like e in a goal containing ctrans e x
Class CDestrSubstGoal (P : Prop) (Q : Prop) :=
  cdestr_subst_goal {cdestruct_subst_goal : Q}.
Global Hint Mode CDestrSubstGoal ! - : typeclass_instances.
Arguments cdestr_subst_goal {_ _} _.
Arguments cdestruct_subst_goal _ {_ _}.
Ltac get_cdestr_subst_goal_evars _ :=
  lazymatch goal with
  | |- CDestrSubstGoal ?G _ ⇒ G
  end.

If CDestrMatchT is enabled for a type, then cdestruct will process match cases of that type by calling destruct on the match discriminee. The value will therefore be destructed even if not directly processed by cdestruct
#[local] Set Typeclasses Strict Resolution.
Class CDestrMatchT (T : Type) := {}.
#[local] Unset Typeclasses Strict Resolution.

CDestrMatch is CDestrMatch T for all T
Class CDestrMatch := {}.
Global Instance cdestr_matchT `{CDestrMatch} T : CDestrMatchT T. Qed.

If CDestrMatchNoEq is enabled for a type, then whenever CDestruct destroy the discriminee of a match with that type, it does not generate the corresponding equality, this is intended for types like {P} + {Q}
#[local] Set Typeclasses Strict Resolution.
Class CDestrMatchNoEq (T : Type) := {}.
#[local] Unset Typeclasses Strict Resolution.

CDestrRecInj allow cdestruct to blow up record equalities of the form {| ... |} = {| ... |} in a group of field-wise equality. One must specify the constructor term for internal reasons (it's hard to guess). The record must implement Settable
#[local] Set Typeclasses Strict Resolution.
Class CDestrRecInj (rec_type : Type) {constr_type : Type}
  (constr : constr_type) := {}.
#[local] Unset Typeclasses Strict Resolution.

Directed rewriting. Declares that if A = B, then rewriting A to B is a good idea, This is not used by default as it is quite fragile, probably best use only as a local hint.
This is really fragile and might be deleted, use with care
#[local] Set Typeclasses Strict Resolution.
Class CDestrDRew {T} (A : T) (B : T) := {}.
#[local] Unset Typeclasses Strict Resolution.

CDestruct helper tactics

Breaking up match cases

Breaks any match case found in p according to the typeclass options
Ltac2 break_match_in p :=
  lazy_match! p with
  | context [match inspect ?b with _ ⇒ _ end] ⇒
      let t := Constr.type b in
      assert_option (CDestrMatchT $t);
      Std.case false ('(inspect $b), Std.NoBindings);
      let hb := intro_get_name () in
      Std.case false (Control.hyp hb, Std.NoBindings);
      clear $hb
  | context [match ?b with _ ⇒ _ end] ⇒
      let t := Constr.type b in
      assert_option (CDestrMatchT $t);
      if has_option (CDestrMatchNoEq $t)
      then Std.case false (b, Std.NoBindings)
      else
        ltac1:(b |- case_eq b) (Ltac1.of_constr b)
  end.

Substitution

If the provided constr is a variable, calls subst on it, otherwise backtracks
Ltac2 subst_constr x := let x := get_var_bt x in Std.subst [x].

subst_clean h x substitute x using equality h after reverting all hypotheses using x, This insured that all hypotheses modified by the substitution are back in the goal
Ltac2 subst_clean h x :=
  move $h before $x;
  revert dependent $x;
  intros $x $h;
  Std.subst [x].

Decide if h1 is before h2 in the current goal
Ltac2 hyp_before h1 h2 :=
  Ident.equal h1
    (Control.hyps ()
     |> List.map (fun (h, _, _) ⇒ h)
     |> List.find (fun h ⇒ Ident.equal h h1 || Ident.equal h h2)).

Check if substitution is allowed, which means that the variable to be substitued is below HypBlock.
Ltac2 can_subst x :=
  match get_hyp_id pat:(hyp_block) with
  | Some hb ⇒ hyp_before hb x
  | None ⇒ true
  end.

Ltac2 clean_up_eq h x y :=
  match get_var x, get_var y with
  | Some x, Some y ⇒
      
      if hyp_before x y
      then (assert_bt (can_subst y); subst_clean h y)
      else (assert_bt (can_subst x); subst_clean h x)
  | Some x, None ⇒ assert_bt (can_subst x); subst_clean h x
  | None, Some y ⇒ assert_bt (can_subst y); subst_clean h y
  | None, None ⇒ Control.zero Match_failure
  end.

Blocking

We need an actually opaque block, so we make a new one
Definition cblock {A : Type} (a : A) := a.
Opaque cblock.

Ltac2 cblock_goal0 () := lazy_match! goal with [ |- ?t ] ⇒ change (cblock $t) end.
Ltac2 Notation cblock_goal := cblock_goal0 ().
Ltac2 uncblock_goal0 () := cbv [cblock].
Ltac2 Notation uncblock_goal := uncblock_goal0 ().

cdestruct_step can block an hypothesis if need to be simplified, but it is used in a dependent manner (e.g. in a transport call). In this case the hypotheses would be duplicated and the original is blocked. At the end, blocked hypotheses must thus be cleared if they are not longer needed, or otherwise unblocked
Ltac2 clear_or_uncblock h :=
  clear $h ||ₜ cbv [cblock] in $h.
Ltac2 clear_or_uncblock_hyp () :=
  match! goal with
  | [h : cblock _ |- _] ⇒ clear_or_uncblock h
  end.
Ltac2 clear_or_uncblock_hyps () := repeat (clear_or_uncblock_hyp ()).

CDestruct Step

cdestruct works by repeating one single simplification step until it doesn't work (or doesn't make progress) Therefore there is no transmission of information between the steps, except what is in the goal and what is in the context. The general idea being that hypotheses to be processes are in the goal, and hypotheses already processed are in the context.
Core cdestruct engine: One single step
#[warnings="-ltac2-unused-variable"]
Ltac2 cdestruct_step0 () :=
  match! goal with
  | [|- ∀ _ : ?t, _] ⇒
      assert_option (CDestrCase $t);
      let h := intro_get_name () in
      Std.case false (Control.hyp h, Std.NoBindings);
      clear $h
  
  
  
  
  | [|- ?t = ?t → _ ] ⇒ intros _
  | [|- ∀ _ : ?t = ?t, _ ] ⇒ refine '(simplification_K _ $t _ _)
  | [|- ∀ _ : _, _ ] ⇒
      let h := intro_get_name () in
      progress (cbn in $h);
      revert $h
  | [|- ∀ _ : ?p, _] ⇒
      let r := '(@cdestruct_simpl false $p _
                   ltac:(block_all_evars get_cdestr_simpl_evars; tc_solve)) in
      let r := eval cbv[blocked_evar] in $r in
      let h := intro_get_name () in
      orelse
      (fun () ⇒ apply (iffLR $r) in $h; revert $h)
      (fun _ ⇒
         
         let h' := pose_proof_get (Control.hyp h) in
         apply (iffLR $r) in $h';
         revert $h';
         change (cblock $p) in $h;
         revert $h)
  | [|- ∀ _ : ?p, _ ] ⇒
      let cds := '(@cdestruct_subst $p _
                     ltac:(block_all_evars get_cdestr_subst_evars; tc_solve)) in
      let cds := eval cbv[blocked_evar] in $cds in
      let h := intro_get_name () in
      let prf := Control.hyp h in
      let e := pose_proof_get '($cds $prf) in
      cbn in $e;
      lazy_match! Constr.type (Control.hyp e) with
      | ?x = ?y ⇒ clean_up_eq e x y
      end;
      try (revert $h)
  | [|- ∀ _ : ?x = ?y, _ ] ⇒
      
      assert_option (CDestrDRew $x $y);
      let h := intro_get_name () in
      let t := Control.hyp h in
      progress (setoid_rewrite $t);
      revert $h
  | [|- ∀ _ : ?p, _ ] ⇒ break_match_in p

  
  | [_ : ?h |- ?h → _] ⇒ intros _
  
  | [h2 : ?h → _ |- ?h → _] ⇒
      let hn := intro_get_name () in
      assert_bt (can_subst h2);
      revert $h2; revert $hn
 
  | [|- ∀ _ : _, _] ⇒ intro

  
  | [|- cblock _] ⇒ ()

  | [|- ¬ ?h ] ⇒ change (¬ _) with ($h → False)
  
  | [|- ?t ] ⇒ assert_option (CDestrSplit $t); split
  | [|- _] ⇒ apply obv_true
  | [|- _] ⇒ progress cbn
  | [|- @eq (∀ _, _) _ _] ⇒ apply functional_extensionality_dep
  | [|- ?p] ⇒
      let r := '(@cdestruct_simpl true $p _
                   ltac:(block_all_evars get_cdestr_simpl_evars; tc_solve)) in
      let r := eval cbv[blocked_evar] in $r in
      apply (iffRL $r)
  | [|- ?p] ⇒
      let e :=
        pose_proof_get
          '(@cdestruct_subst_goal $p _
              ltac:(block_all_evars get_cdestr_subst_goal_evars; tc_solve)) in
      unblock_evars;
      cbn in $e;
      lazy_match! Constr.type (Control.hyp e) with
      | ?x = ?y ⇒ clean_up_eq e x y
      end
  | [|- ?p] ⇒ break_match_in p
  end.

Ltac2 Notation cdestruct_step := cdestruct_step0 ().
Ltac cdestruct_step := ltac2:(cdestruct_step).

CDestruct top-level setup and syntax

The core of cdestruct is just cdestruct_steps = repeat cdestruct_step, however we also want to do some pre and post processing, to give a nice UX.
First we delimit the range of hypotheses (and maybe goal) that we need to process:
  • We need to revert all hypotheses to process
  • We need to block the part of the goal we do not want to process
  • We add a marker (hyp_block) to mark the set hypotheses we can change, anything above should be left untouched
Repeat a single cdestruct step
Ltac2 Notation cdestruct_steps := repeat (once cdestruct_step).
Ltac cdestruct_steps := ltac2:(cdestruct_steps).

Preprocessing tactics

Remove the hyp_block or fails otherwise
Ltac2 clear_hyp_block0 () :=
  Control.enter
    (fun () ⇒
       match get_hyp_id pat:(hyp_block) with
       | Some h ⇒ Std.clear [h]
       | None ⇒ throw_tacticf "clear_hyp_block: HypBlock not found"
    end).
Ltac2 Notation clear_hyp_block := clear_hyp_block0 ().

Generic cdestruct tactic with goal, hyp and post (clean) processing
Ltac2 cdestruct_gen0 goaltac hyptac cleantac :=
  pose proof HypBlock;
  goaltac ();
  hyptac ();
  cdestruct_steps;
  Control.enter (fun () ⇒ cleantac (); uncblock_goal; clear_or_uncblock_hyps ()).
Ltac2 Notation cdestruct_gen := cdestruct_gen0.

Does intro with a ltac1 pattern
Ltac2 ltac1_intros (pats : Ltac1.t) := ltac1:(pats |- intros pats) pats.

Preprocess for the |- intro_pattern syntax
Ltac2 cdest_intro_start ipats :=
  ltac1_intros ipats; cblock_goal; revert until hyp_block.

Preprocess for the |- ** syntax
Ltac2 cdest_intros_start0 () :=
  intros; cblock_goal; revert until hyp_block.
Ltac2 Notation cdest_intros_start := cdest_intros_start0 ().

Preprocesse the list of hypotheses of cdestruct
Ltac2 cdest_rev_start (l : Ltac1.t) :=
  revert_dependent (ltac1_to_list ltac1_to_ident l).

Postprocess the "as ..." part of cdestruct syntax
Ltac2 cdest_as_end pats :=
  revert until× hyp_block; ltac1_intros pats.

Tactic Notation "cdestruct" hyp_list_sep(hs, ",") :=
  let f := ltac2:(hs |- cdestruct_gen cblock_goal
                          (cdest_rev_start hs) clear_hyp_block)
  in f hs.
Tactic Notation "cdestruct" hyp_list_sep(hs, ",")
                "as" simple_intropattern_list(pats) :=
  let f := ltac2:(hs pats |- cdestruct_gen cblock_goal
                               (cdest_rev_start hs) (cdest_as_end pats))
  in f hs pats.

Tactic Notation "cdestruct" hyp_list_sep(hs, ",")
                "|-" simple_intropattern_list(ipats) :=
  let f := ltac2:(hs ipats |- cdestruct_gen (cdest_intro_start ipats)
                          (cdest_rev_start hs) clear_hyp_block)
  in f hs ipats.
Tactic Notation "cdestruct" hyp_list_sep(hs, ",")
                "|-" simple_intropattern_list(ipats)
                "as" simple_intropattern_list(pats) :=
  let f := ltac2:(hs ipats pats |- cdestruct_gen (cdest_intro_start ipats)
                               (cdest_rev_start hs) (cdest_as_end pats))
  in f hs ipats pats.


Tactic Notation "cdestruct" hyp_list_sep(hs, ",") "|-" "**" :=
  let f := ltac2:(hs |- cdestruct_gen cdest_intros_start
                          (cdest_rev_start hs) clear_hyp_block)
  in f hs.
Tactic Notation "cdestruct" hyp_list_sep(hs, ",") "|-" "**"
                "as" simple_intropattern_list(pats) :=
  let f := ltac2:(hs pats |- cdestruct_gen cdest_intros_start
                               (cdest_rev_start hs) (cdest_as_end pats))
  in f hs pats.

Tactic Notation "cdestruct" hyp_list_sep(hs, ",") "|-" "***" :=
  let f := ltac2:(hs |- cdestruct_gen ()
                          (cdest_rev_start hs) clear_hyp_block)
  in f hs.
Tactic Notation "cdestruct" hyp_list_sep(hs, ",") "|-" "***"
                "as" simple_intropattern_list(pats) :=
  let f := ltac2:(hs pats |- cdestruct_gen ()
                               (cdest_rev_start hs) (cdest_as_end pats))
  in f hs pats.

Default Instanciation of the CDestruct typeclass options

Inductive case splitting

Enable default rules that can split a goal, like case splitting ∨ or goal splitting ∧
Class CDestrSplitGoal := {}.

CDestruct destroys ∧, ∃, pairs, True, False,unit and Empty_set by default. It purposefully does NOT destroy ∨ and + by default. This behaviour can be added locally with CDestrSplitGoal
#[global] Instance cdestruct_and A B : CDestrCase (A ∧ B) := ltac:(constructor).
#[global] Instance cdestruct_ex T P : CDestrCase (∃ x : T, P x) := ltac:(constructor).
#[global] Instance cdestruct_sigT T (F : T → Type) :
  CDestrCase (sigT F) := ltac:(constructor).
#[global] Instance cdestruct_pair (A B : Type) :
  CDestrCase (A × B) := ltac:(constructor).
#[global] Instance cdestruct_True : CDestrCase True := ltac:(constructor).
#[global] Instance cdestruct_False : CDestrCase False := ltac:(constructor).
#[global] Instance cdestruct_or `{CDestrSplitGoal} A B :
  CDestrCase (A ∨ B) := ltac:(constructor).
#[global] Instance cdestruct_sum `{CDestrSplitGoal} A B :
  CDestrCase (A + B) := ltac:(constructor).
#[global] Instance cdestruct_unit : CDestrCase () := ltac:(constructor).
#[global] Instance cdestruct_Empty_set : CDestrCase Empty_set := ltac:(constructor).

CDestruct can split goals if enabled by CDestrSplitGoal
#[global] Instance cdestr_split_and `{CDestrSplitGoal}
  A B : CDestrSplit (A ∧ B) := ltac:(constructor).
#[global] Instance cdestr_split_iff `{CDestrSplitGoal}
  A B : CDestrSplit (A ↔ B) := ltac:(constructor).
#[global] Instance cdestr_split_True : CDestrSplit True := ltac:(constructor).
#[global] Instance cdestr_split_unit : CDestrSplit () := ltac:(constructor).

Match case splitting

For some case spliting on match cases, we not want to keep the equalities
#[global] Instance cdestruct_match_noeq_sig A (P : A → Prop)
  : CDestrMatchNoEq (sig P) := ltac:(constructor).
#[global] Instance cdestruct_match_noeq_sumbool P Q
  : CDestrMatchNoEq ({P} + {Q}) := ltac:(constructor).

ObvFalse simplification

Obviously False equality are simplified to False
TODO: with contradiction in ObvFalse this might be weird
Global Instance cdestruct_obvFalse b (P : Prop) `{ObvFalse P} :
  CDestrSimpl b (P : Prop) False.
Proof. constructor. by destruct H. Qed.

Injectivity

Injective equalities are simplified by default, up to 4 arguments, both in the hypotheses and the goal
Global Instance cdestruct_inj b `{Inj A B RA RB f} {HP: Proper (RA ==> RB) f} x y :
  CDestrSimpl b (RB (f x) (f y)) (RA x y).
Proof. constructor. apply (inj_iff f). Qed.

Global Instance cdestruct_inj2 b `{Inj2 A B C RA RB RC f}
  `{!Proper (RA ==> RB ==> RC) f} x1 x2 y1 y2 :
  CDestrSimpl b (RC (f x1 x2) (f y1 y2)) (RA x1 y1 ∧ RB x2 y2).
Proof. constructor. apply (inj2_iff f). Qed.

Global Instance cdestruct_inj3 b `{Inj3 A B C D R1 R2 R3 RS f}
    {HP : Proper (R1 ==> R2 ==> R3 ==> RS) f} x1 x2 x3 y1 y2 y3 :
  CDestrSimpl b (RS (f x1 x2 x3) (f y1 y2 y3)) (R1 x1 y1 ∧ R2 x2 y2 ∧ R3 x3 y3).
Proof. constructor. apply (inj3_iff f). Qed.

Global Instance cdestruct_inj4 b `{Inj4 A B C D E R1 R2 R3 R4 RS f}
    {HP : Proper (R1 ==> R2 ==> R3 ==> R4 ==> RS) f} x1 x2 x3 x4 y1 y2 y3 y4 :
  CDestrSimpl b (RS (f x1 x2 x3 x4) (f y1 y2 y3 y4))
    (R1 x1 y1 ∧ R2 x2 y2 ∧ R3 x3 y3 ∧ R4 x4 y4).
Proof. constructor. apply (inj4_iff f). Qed.

Implementation of CDestrRecInj for record injectivity, see that typeclass definition for an explanation
#[global] Hint Extern 30 (CDestrSimpl _ (?L =@{?T} ?R) ?Q) ⇒
  let L_head := get_head L in
  let R_head := get_head R in
  has_option (CDestrRecInj T L_head);
  unify L_head R_head;
  constructor;
  rewrite record_eq_unfold;
  cbn;
  reflexivity : typeclass_instances.

Substitution


#[global] Hint Extern 10 (CDestrSubst (?x = ?y) _) ⇒
  (first [is_var x | is_var y]; assert_fails (unify x y); econstructor; let H := fresh "H" in intro H; exact H)
  : typeclass_instances.

Ltac cds_by_congruence Ht :=
  constructor;
  let Hs := fresh "H" in
  intro Hs;
  class_apply (@cdestruct_subst Ht);[clear Hs| congruence].

#[global] Hint Extern 5 (CDestrSubst (?f ?x = ?f ?y) _) ⇒
  (assert_fails (unify x y);
   cds_by_congruence (x = y)) : typeclass_instances.

#[global] Hint Extern 4 (CDestrSubst (?f ?x _ = ?f ?y _) _) ⇒
  (assert_fails (unify x y);
   cds_by_congruence (x = y)) : typeclass_instances.

#[global] Hint Extern 3 (CDestrSubst (?f ?x _ _ = ?f ?y _ _) _) ⇒
  (assert_fails (unify x y);
   cds_by_congruence (x = y)) : typeclass_instances.

#[global] Hint Extern 2 (CDestrSubst (?f ?x _ _ _ = ?f ?y _ _ _)) ⇒
  (assert_fails (unify x y);
   cds_by_congruence (x = y)) : typeclass_instances.

CTrans simplification and substitution

Hint Extern 5 (CDestrSimpl _ ?P _) ⇒
       match P with
       | context [ctrans] ⇒
           constructor;
           progress (simp ctrans);
           reflexivity
       end : typeclass_instances.

Hint Extern 9 (CDestrSubst ?P _) ⇒
       match P with
       | context [@ctrans _ _ _ ?A ?B ?E _] ⇒
           assert_fails (unify A B);
           constructor;
           intros _;
           let t := type of E in
           let t' := eval cbn in t in
           class_apply (@cdestruct_subst t');[ | exact E]
           
       end : typeclass_instances.

Hint Extern 9 (CDestrSubstGoal ?P _) ⇒
       match P with
       | context [@ctrans _ _ _ ?A ?B ?E _] ⇒
           assert_fails (unify A B);
           constructor;
           let t := type of E in
           let t' := eval cbn in t in
             class_apply (@cdestruct_subst t');[ | exact E]
       end : typeclass_instances.

JMeq simplification


Global Instance cdestruct_JMeq b A (x y : A) :
  CDestrSimpl b (x =ⱼ y) (x = y).
Proof. constructor. use JMeq_eq. naive_solver. Qed.

Global Instance cdestruct_neg_JMeq b A (x y : A) :
  CDestrSimpl b (x ≠ⱼ y) (x ≠ y).
Proof. constructor. use JMeq_eq. naive_solver. Qed.

bool_decide simplification

Instance cdestruct_bool_decide_true b `{Decision P} :
  CDestrSimpl b (bool_decide P = true) P.
Proof. tcclean. apply bool_decide_eq_true. Qed.

Instance cdestruct_bool_decide b `{Decision P} :
  CDestrSimpl b (bool_decide P) P.
Proof. tcclean. apply bool_decide_spec. Qed.

Instance cdestruct_bool_decide_false b `{Decision P} :
  CDestrSimpl b (bool_decide P = false) (¬ P).
Proof. tcclean. apply bool_decide_eq_false. Qed.

Logical connectives simplification


Instance cdestruct_impl_simpl b P Q :
  TCFastDone P → CDestrSimpl b (P → Q) Q.
Proof. tcclean. naive_solver. Qed.

Instance cdestruct_not_not b P :
  CDestrSimpl b (¬ ¬ P) P.
Proof. tcclean. use NNPP. naive_solver. Qed.

Instance cdestruct_not_and_or_ctxt P Q :
  CDestrSimpl false (¬ (P ∧ Q)) (¬ P ∨ ¬ Q).
Proof. tcclean. tauto. Qed.

Instance cdestruct_not_and_or_goal P Q :
  CDestrSimpl true (¬ P ∨ ¬ Q) (¬ (P ∧ Q)) | 10.
Proof. tcclean. tauto. Qed.

Instance cdestruct_not_or_l_goal P Q :
  CDestrSimpl true (¬ P ∨ Q) (P → Q) | 20.
Proof. tcclean. tauto. Qed.

Instance cdestruct_not_or_r_goal P Q :
  CDestrSimpl true (P ∨ ¬ Q) (Q → P) | 20.
Proof. tcclean. tauto. Qed.

Instance cdestruct_not_or_and b P Q :
  CDestrSimpl b (¬ (P ∨ Q)) (¬ P ∧ ¬ Q).
Proof. tcclean. naive_solver. Qed.

Instance cdestruct_or_False_l b P :
  CDestrSimpl b (False ∨ P) P.
Proof. tcclean. naive_solver. Qed.

Instance cdestruct_or_False_r b P :
  CDestrSimpl b (P ∨ False) P.
Proof. tcclean. naive_solver. Qed.

Instance cdestruct_and_True_l b P :
  CDestrSimpl b (True ∧ P) P.
Proof. tcclean. naive_solver. Qed.

Instance cdestruct_and_True_r b P :
  CDestrSimpl b (P ∧ True) P.
Proof. tcclean. naive_solver. Qed.

Set handling

Import this module to make CDestruct do set unfolding automatically. For now only in the x ∈ C case
Module CDestrUnfoldElemOf.
  Instance cdestr_unfold_elem_of b `{ElemOf A C} (x : A) (S : C) P:
    SetUnfoldElemOf x S P →
    Unconvertible Prop (x ∈ S) P →
    CDestrSimpl b (x ∈ S) P.
  Proof. by tcclean. Qed.
  Hint Mode SetUnfoldElemOf + + + + ! - : typeclass_instances.
End CDestrUnfoldElemOf.