Destruct Tactic

Stream: metaprogramming / tactics

[Chase Norman]

New destruct tactic

destruct is a new tactic which eliminates structure types from the local context and goal, by unpacking them. It comes pre-packaged with Canonical, and powers its new encoding of structure types.

You can use destruct to skolemize existentials:

import Canonical

example (p : ∃ x : Nat, x = x + 1) : False := by
  destruct
  /-
  p_w : Nat
  p_h : p_w = p_w + 1
  -/

destruct can unpack nested structures:

variable (A B C : Prop)
example (p : (A ↔ B) ∧ C) : False := by
  destruct
  /-
  p_left_mp : A → B
  p_left_mpr : B → A
  p_right : C
  -/

destruct can even unpack structure types that are behind universal quantifiers, implications, and function types. Observe how each field has A as an antecedent, and only the right field has B:

example (p : A → (B ∧ (B → C))) : False := by
  destruct
  /-
  p_left : A → B
  p_right : A → B → C
  -/

But wait, there's more. You can even unpack structures in the antecedents of premises:

example (p : (Nat × Nat) → (Nat × Nat)) : Nat := by
  destruct
  /-
  p_fst p_snd : Nat → Nat → Nat
  -/

If the goal is a structure type, multiple goals can be created:

example : ∃ n : Nat, n = n := by
  destruct
  /- 2 goals
  ⊢ Nat
  ⊢ ?m.476 = ?m.476
  -/

There is a default list of structures that unfold, but you can specify your own:

example (map : Std.HashMap String Nat) : Nat := by
  destruct [Std.HashMap, Std.DHashMap, Std.DHashMap.Raw]
  /-
  map_inner_inner_size : Nat
  map_inner_inner_buckets_toList : List (Std.DHashMap.Internal.AssocList String fun x ↦ Nat)
  map_inner_wf : { size := map_inner_inner_size, buckets := { toList := map_inner_inner_buckets_toList } }.WF
  -/

Unit is treated like a structure, and is eliminated. Also notice the treatment of dependence on variables that were previously structure types:

example (p : (Unit × Unit ×' ∃ x : (Nat × Nat), x.1 = x.2) → (A → B)) : B := by
  destruct
  /-
  ∀ (a_snd_snd_w_fst a_snd_snd_w_snd : Nat),
  (a_snd_snd_w_fst, a_snd_snd_w_snd).fst = (a_snd_snd_w_fst, a_snd_snd_w_snd).snd → A → B
  -/

While structure types can be useful for encapsulation, if the structure is intended to be used it is often best to unfold it for the purposes of automation and compilation. With destruct this transformation can be done automatically.