lean4-htt/tests/elab/casesOnSameCtor.lean

import Lean

/-! This tests and documents the constructions in CasesOnSameCtor. -/

open Lean Meta

inductive Vec (α : Type u) : Nat → Type u
  | nil  : Vec α 0
  | cons : α → {n : Nat} → Vec α n → Vec α (n+1)

namespace Vec

-- set_option debug.skipKernelTC true
run_meta mkCasesOnSameCtor `Vec.match_on_same_ctor ``Vec

/--
info: Vec.match_on_same_ctor.het.{u_1, u} {α : Type u} {motive : {a : Nat} → Vec α a → {a : Nat} → Vec α a → Sort u_1}
  {a✝ : Nat} (t : Vec α a✝) {a✝¹ : Nat} (t✝ : Vec α a✝¹) (h : t.ctorIdx = t✝.ctorIdx) (nil : motive nil nil)
  (cons :
    (a : α) →
      {n : Nat} → (a_1 : Vec α n) → (a_2 : α) → {n_1 : Nat} → (a_3 : Vec α n_1) → motive (cons a a_1) (cons a_2 a_3)) :
  motive t t✝
-/
#guard_msgs in
#check Vec.match_on_same_ctor.het

/--
info: Vec.match_on_same_ctor.{u_1, u} {α : Type u}
  {motive : {a : Nat} → (t t_1 : Vec α a) → t.ctorIdx = t_1.ctorIdx → Sort u_1} {a✝ : Nat} (t t✝ : Vec α a✝)
  (h : t.ctorIdx = t✝.ctorIdx) (nil : Unit → motive nil nil ⋯)
  (cons : (a : α) → {n : Nat} → (a_1 : Vec α n) → (a' : α) → (a'_1 : Vec α n) → motive (cons a a_1) (cons a' a'_1) ⋯) :
  motive t t✝ h
-/
#guard_msgs in
#check Vec.match_on_same_ctor

-- Splitter and equations are generated
/--
info: Vec.match_on_same_ctor.splitter.{u_1, u} {α : Type u}
  {motive : {a : Nat} → (t t_1 : Vec α a) → t.ctorIdx = t_1.ctorIdx → Sort u_1} {a✝ : Nat} (t t✝ : Vec α a✝)
  (h : t.ctorIdx = t✝.ctorIdx) (nil : Unit → motive nil nil ⋯)
  (cons : (a : α) → {n : Nat} → (a_1 : Vec α n) → (a' : α) → (a'_1 : Vec α n) → motive (cons a a_1) (cons a' a'_1) ⋯) :
  motive t t✝ h
-/
#guard_msgs in
#check Vec.match_on_same_ctor.splitter

-- After #11211 this is no longer true. Should we thunk the same-ctor-construction?

-- -- Since there is no overlap, the splitter is equal to the matcher
-- -- (I wonder if we should use this in general in MatchEq)
-- example : @Vec.match_on_same_ctor = @Vec.match_on_same_ctor.splitter := by rfl

/--
info: Vec.match_on_same_ctor.eq_2.{u_1, u} {α : Type u}
  {motive : {a : Nat} → (t t_1 : Vec α a) → t.ctorIdx = t_1.ctorIdx → Sort u_1} (a✝ : α) (n : Nat) (a✝¹ : Vec α n)
  (a'✝ : α) (a'✝¹ : Vec α n) (nil : Unit → motive nil nil ⋯)
  (cons : (a : α) → {n : Nat} → (a_1 : Vec α n) → (a' : α) → (a'_1 : Vec α n) → motive (cons a a_1) (cons a' a'_1) ⋯) :
  (match n + 1, Vec.cons a✝ a✝¹, Vec.cons a'✝ a'✝¹ with
    | 0, Vec.nil, Vec.nil, ⋯ => nil ()
    | n + 1, Vec.cons a a_1, Vec.cons a' a'_1, ⋯ => cons a a_1 a' a'_1) =
    cons a✝ a✝¹ a'✝ a'✝¹
-/
#guard_msgs in
#check Vec.match_on_same_ctor.eq_2

-- Recursion works

-- set_option trace.split.debug true
-- set_option trace.split.failure true
-- set_option trace.Elab.definition.structural.eqns true

def decEqVec {α} {a} [DecidableEq α] (x : @Vec α a) (x_1 : @Vec α a) : Decidable (x = x_1) :=
  if h : Vec.ctorIdx x = Vec.ctorIdx x_1 then
    Vec.match_on_same_ctor x x_1 h (fun _ => isTrue rfl)
      @fun a_1 _ a_2 b b_1 =>
        if h_1 : @a_1 = @b then by
          subst h_1
          exact
            let inst := decEqVec @a_2 @b_1;
            if h_2 : @a_2 = @b_1 then by subst h_2; exact isTrue rfl
            else isFalse (by intro n; injection n; apply h_2 _; assumption)
        else isFalse (by intro n_1; injection n_1; apply h_1 _; assumption)
  else isFalse (fun h' => h (congrArg Vec.ctorIdx h'))
termination_by structural x


-- Equation generation and pretty match syntax:

/--
info: theorem Vec.decEqVec.eq_def.{u_1} : ∀ {α : Type u_1} {a : Nat} [inst : DecidableEq α] (x x_1 : Vec α a),
  x.decEqVec x_1 =
    if h : x.ctorIdx = x_1.ctorIdx then
      match a, x, x_1 with
      | 0, Vec.nil, Vec.nil, ⋯ => isTrue ⋯
      | x + 1, Vec.cons a_1 a_2, Vec.cons b b_1, ⋯ =>
        if h_1 : a_1 = b then
          h_1 ▸
            have inst_1 := a_2.decEqVec b_1;
            if h_2 : a_2 = b_1 then
              h_2 ▸
                have inst := a_2.decEqVec a_2;
                isTrue ⋯
            else isFalse ⋯
        else isFalse ⋯
    else isFalse ⋯
-/
#guard_msgs(pass trace, all) in
#print sig decEqVec.eq_def


-- Incidentally, normal match syntax is able to produce an equivalent matcher
-- (with different implementation):
-- (see #10195 for problems with equation generation)

def decEqVecPlain {α} {a} [DecidableEq α] (x : @Vec α a) (x_1 : @Vec α a) : Decidable (x = x_1) :=
  if h : Vec.ctorIdx x = Vec.ctorIdx x_1 then
    match x, x_1, h with
    | Vec.nil, Vec.nil, _ => isTrue rfl
    | Vec.cons a_1 a_2, Vec.cons b b_1, _ =>
        if h_1 : @a_1 = @b then by
          subst h_1
          exact
            let inst := decEqVecPlain @a_2 @b_1;
            if h_2 : @a_2 = @b_1 then by subst h_2; exact isTrue rfl
            else isFalse (by intro n; injection n; apply h_2 _; assumption)
        else isFalse (by intro n_1; injection n_1; apply h_1 _; assumption)
  else isFalse (fun h' => h (congrArg Vec.ctorIdx h'))
termination_by structural x
end Vec

namespace List
-- set_option debug.skipKernelTC true


-- No code is generated for the match_on_same_ctor or match_on_same_ctor.het
/--
trace: [Compiler.saveMono] size: 5
    def _private.elab.casesOnSameCtor.0._eval._lam_0 _x.1 _x.2 _x.3 _y.4 @&_y.5 @&_y.6 @&_y.7 @&_y.8 @&_y.9 _y.10 : EST.Out
      Exception lcAny PUnit :=
      let _x.11 := mkCasesOnSameCtor _x.1 _x.2 _y.6 _y.7 _y.8 _y.9 _y.10;
      cases _x.11 : EST.Out Exception lcAny PUnit
      | EST.Out.ok a.12 a.13 =>
        let _x.14 := @EST.Out.ok ◾ ◾ ◾ _x.3 a.13;
        return _x.14
      | EST.Out.error a.15 a.16 =>
        return _x.11
[Compiler.saveMono] size: 7
    def _private.elab.casesOnSameCtor.0._eval @&a @&a a.1 : EST.Out Exception lcAny PUnit :=
      let _x.2 := "List";
      let _x.3 := "match_on_same_ctor";
      let _x.4 := Name.mkStr2 _x.2 _x.3;
      let _x.5 := Name.mkStr1 _x.2;
      let _x.6 := PUnit.unit;
      let _f.7 := _eval._lam_0 _x.4 _x.5 _x.6;
      let _x.8 := Lean.Elab.Command.liftTermElabM._redArg _f.7 a a a.1;
      return _x.8
-/
#guard_msgs in
set_option trace.Compiler.saveMono true in
run_meta mkCasesOnSameCtor `List.match_on_same_ctor ``List

/--
info: List.match_on_same_ctor.{u_1, u} {α : Type u} {motive : (t t_1 : List α) → t.ctorIdx = t_1.ctorIdx → Sort u_1}
  (t t✝ : List α) (h : t.ctorIdx = t✝.ctorIdx) (nil : Unit → motive [] [] ⋯)
  (cons : (head : α) → (tail : List α) → (head' : α) → (tail' : List α) → motive (head :: tail) (head' :: tail') ⋯) :
  motive t t✝ h
-/
#guard_msgs in
#check List.match_on_same_ctor

end List

namespace BadIdx
opaque f : Nat → Nat
inductive T : (n : Nat) → Type where
  | mk1 : Fin n → T (f n)
  | mk2 : Fin (2*n) → T (f n)

run_meta mkCasesOnSameCtorHet `BadIdx.casesOn2Het ``T
/--
error: Dependent elimination failed: Failed to solve equation
  f n✝ = f n
-/
#guard_msgs in
run_meta mkCasesOnSameCtor `BadIdx.casesOn2 ``T

end BadIdx