Knuckledragger Interactive Theorem Prover

The Imp language consists of three main syntactic categories:

1. Arithmetic Expressions (aexp): Includes natural numbers (ANum), variable identifiers (AId), addition (APlus), subtraction (AMinus), and multiplication (AMult).
2. Boolean Expressions (bexp): Includes boolean constants (BTrue, BFalse), equality (BEq), inequality (BNeq), less-than-or-equal (BLe), greater-than (BGt), negation (BNot), and logical AND (BAnd).
3. Commands (com): The executable statements, including CSkip (no-op), CAsgn (assignment x := a), CSeq (sequence c1 ; c2), CIf (conditional if b then c1 else c2 end), and CWhile (loop while b do c end).

Custom notation allows writing these expressions using standard mathematical symbols (e.g., x + y, x <= y, x := y) within the <{ ... }> delimiter.

Inductive aexp : Type :=
  | ANum (n : nat)
  | AId (x : string)
  | APlus (a1 a2 : aexp)
  | AMinus (a1 a2 : aexp)
  | AMult (a1 a2 : aexp).

Inductive bexp : Type :=
  | BTrue
  | BFalse
  | BEq (a1 a2 : aexp)
  | BNeq (a1 a2 : aexp)
  | BLe (a1 a2 : aexp)
  | BGt (a1 a2 : aexp)
  | BNot (b : bexp)
  | BAnd (b1 b2 : bexp).

Inductive com : Type :=
  | CSkip
  | CAsgn (x : string) (a : aexp)
  | CSeq (c1 c2 : com)
  | CIf (b : bexp) (c1 c2 : com)
  | CWhile (b : bexp) (c : com).

The ProofState class is used for interactive, imperative proof construction. It acts as a builder for kd.Proof objects. You start a proof using Lemma(goal).proof() and mutate the state using tactics. Once satisfied, call .qed() to build the final proof.

Key features:

• push() and pop(): Manage a stack of proof states, allowing you to try a tactic and backtrack if it fails.
• intros(): Opens implications or negations, moving the antecedent into the context.
• fixes() / fix(): Opens forall quantifiers.
• simp(): Applies Z3 simplification to the goal or context.
• cases(t): Performs case analysis on a boolean or a datatype constructor.
• auto(): Attempts to discharge the current goal using Z3.

p, q = smt.Bools("p q")

# Interactive workflow
proof = (Lemma(smt.Implies(p, q))
         .push()           # Save state
         .intros()         # Context: [p], Goal: q
         .auto()           # Discharge goal
         .pop()            # Backtrack if needed
         .qed())

Regular expressions can be modeled as an inductive type reg_exp T, where T is the type of characters. This allows you to define a matching relation s =~ re (where s is a list T) using an inductive proposition exp_match.

Key constructors for exp_match include:

• MEmpty: Matches the empty string [] to EmptyStr.
• MChar: Matches a single-element list [x] to Char x.
• MApp: Matches the concatenation of two strings s1 ++ s2 to the application of two regexes App re1 re2.
• MUnionL/MUnionR: Matches a string to either side of a Union.
• MStar0: Matches the empty string to a Star re.
• MStarApp: Matches the concatenation of a string s1 (matching re) and s2 (matching Star re) to Star re.

Inductive reg_exp (T : Type) : Type :=
  | EmptySet
  | EmptyStr
  | Char (t : T)
  | App (r1 r2 : reg_exp T)
  | Union (r1 r2 : reg_exp T)
  | Star (r : reg_exp T).

Inductive exp_match {T} : list T -> reg_exp T -> Prop :=
  | MEmpty : [] =~ EmptyStr
  | MChar x : [x] =~ (Char x)
  | MApp s1 re1 s2 re2 (H1 : s1 =~ re1) (H2 : s2 =~ re2) : (s1 ++ s2) =~ (App re1 re2)
  | MUnionL s1 re1 re2 (H1 : s1 =~ re1) : s1 =~ (Union re1 re2)
  | MUnionR re1 s2 re2 (H2 : s2 =~ re2) : s2 =~ (Union re1 re2)
  | MStar0 re : [] =~ (Star re)
  | MStarApp s1 s2 re (H1 : s1 =~ re) (H2 : s2 =~ (Star re)) : (s1 ++ s2) =~ (Star re)
where "s =~ re" := (exp_match s re).

When writing functions that might fail (e.g., accessing an index in a list that is too short), avoid returning a 'magic' default value like 42. Instead, use an inductive type like natoption to explicitly represent success or failure.

natoption has two constructors:

• Some n: Represents a successful result containing the value n.
• None: Represents a failure or an empty result.

To extract a value from a natoption while providing a fallback, use an elimination pattern (like option_elim).

Inductive natoption : Type :=
  | Some (n : nat)
  | None.

(* Example: nth_error returns Some value if index exists, otherwise None *) 
Fixpoint nth_error (l:natlist) (n:nat) : natoption :=
  match l with
  | nil => None
  | a :: l' => match n with
               | 0 => Some a
               | S n' => nth_error l' n'
               end
  end.

(* Example: option_elim extracts the value or returns a default *) 
Definition option_elim (d : nat) (o : natoption) : nat :=
  match o with
  | Some n' => n'
  | None => d
  end.