ifdef or macro templates

Stream: metaprogramming / tactics

[Kayla Thomas]

Is it possible to put something like C #ifdefs around blocks of code? For example, I have a number of theorems that can apply to both natural deduction and Hilbert style first order logic formulas, and I would like to include those theorems in separate natural deduction and Hilbert proofs without copying and pasting and removing the induction cases that don't apply. My thought was to put #ifdefs around the induction cases that apply to each, and a #define statement in the files that import these common proofs. For example:

-- Hilbert.lean

inductive Formula : Type
  | pred_const_ : PredName → List VarName → Formula
  | pred_var_ : PredName → List VarName → Formula
  | eq_ : VarName → VarName → Formula
  | true_ : Formula
  | not_ : Formula → Formula
  | imp_ : Formula → Formula → Formula
  | forall_ : VarName → Formula → Formula

import Example.lean

-- ND.lean

inductive Formula : Type
  | pred_const_ : PredName → List VarName → Formula
  | pred_var_ : PredName → List VarName → Formula
  | eq_ : VarName → VarName → Formula
  | true_ : Formula
  | false_ : Formula
  | not_ : Formula → Formula
  | imp_ : Formula → Formula → Formula
  | and_ : Formula → Formula → Formula
  | or_ : Formula → Formula → Formula
  | iff_ : Formula → Formula → Formula
  | forall_ : VarName → Formula → Formula
  | exists_ : VarName → Formula → Formula

#define ND
import Example.lean

-- Example.lean

lemma blah
  ...
  (F : Formula) :
  ... :=
  by
  induction F
  case pred_const_ X xs | pred_var_ X xs =>
    ...
  case eq_ x y =>
    ...
  case
    true_
    -- ifdef ND
    | false_
    -- endif
  =>
    ...
  case not_ _ phi_ih =>
    ...
  case
    imp_ phi psi phi_ih psi_ih
    -- ifdef ND
    | and_ phi psi phi_ih psi_ih
    | or_ phi psi phi_ih psi_ih
    | iff_ phi psi phi_ih psi_ih
    -- endif
  =>
    ...
  case
    forall_ x phi phi_ih
    -- ifdef ND
    | exists_ x phi phi_ih
    -- endif
  =>
    ...

[Kayla Thomas]

I realize that the logic doesn't work with the imports, but I hope it describes the problem I am trying to solve.

[Kayla Thomas]

I suppose one could replace the imports with calls to some kind of macro template?