(* Basic proof structure *)
Theorem example : forall n : nat, n + 0 = n.
Proof.
  induction n.
  - (* Base case: n = 0 *) reflexivity.
  - (* Inductive case: n = S n' *)
    simpl.
    rewrite IHn.
    reflexivity.
Qed.

(* Common tactics *)
- intros      : Introduce hypotheses
- destruct    : Case analysis
- induction   : Induction
- rewrite     : Rewrite using equality
- apply       : Apply lemma
- exact       : Provide exact term
- reflexivity : Prove equality
- simpl       : Simplify
- unfold      : Unfold definition
- rewrite     : Rewrite
- assert      : Make assertion
- remember    : Remember expression
- generalize  : Generalize over term

(* Define list reversal *)
Fixpoint rev {A : Type} (l : list A) : list A :=
  match l with
  | nil => nil
  | cons x xs => rev xs ++ cons x nil
  end.

(* Prove correctness *)
Theorem rev_correct : forall A (l : list A),
  rev (rev l) = l.
Proof.
  induction l as [| x xs IH ].
  - (* Base case: l = nil *) reflexivity.
  - (* Inductive case *)
    simpl.
    rewrite <- IH.
    rewrite <- app_assoc.
    simpl.
    reflexivity.
Qed.

(* More efficient version with accumulator *)
Fixpoint rev_append {A : Type} (l acc : list A) : list A :=
  match l with
  | nil => acc
  | cons x xs => rev_append xs (cons x acc)
  end.

Definition rev' {A : Type} (l : list A) := rev_append l nil.

Lemma rev_append_rev : forall A (l acc : list A),
  rev_append l acc = rev l ++ acc.
Proof.
  induction l; intros.
  - simpl. reflexivity.
  - simpl. rewrite IHl. rewrite app_assoc. reflexivity.
Qed.

(* BST definition *)
Inductive bst (key : Set) (R : key -> key -> Prop) : key -> Prop :=
  | bst_empty : bst key R EmptyKey
  | bst_node : forall k v l r,
      bst key R l ->
      bst key R r ->
      (forall k', In key l k' -> R k' k) ->
      (forall k', In key r k -> R k k') ->
      bst key R k.

(* Insert preserves BST *)
Lemma bst_insert_preserves : forall key R (H: StrictOrder R) 
  k v (t : bst key R k),
  bst key R (insert k v t).
Proof.
  induction t; intros.
  - constructor; auto.
  - destruct (compare_dec k0 k) as [H'|H'|H'].
    + (* k < k0: insert in left *)
      constructor; auto.
      * apply IHt1; auto.
      * intros. apply H1. left; auto.
    + (* k = k0: replace *)
      constructor; auto.
    + (* k > k0: insert in right *)
      constructor; auto.
      * apply IHt2; auto.
      * intros. apply H1. right; auto.
Qed.

(* Simple expression language *)
Inductive expr : Type :=
  | EConst : nat -> expr
  | EPlus : expr -> expr -> expr
  | EVar : nat -> expr.

(* Target: stack machine *)
Inductive instr : Type :=
  | IPush : nat -> instr
  | IAdd : instr
  | ILoad : nat -> instr.

Definition prog := list instr.

(* Compiler *)
Fixpoint compile (e : expr) : prog :=
  match e with
  | EConst n => IPush n :: nil
  | EPlus e1 e2 => compile e2 ++ compile e1 ++ IAdd :: nil
  | EVar x => ILoad x :: nil
  end.

(* Compiler correctness *)
Inductive stack : Type := stack (l : list nat).

Inductive exec : prog -> stack -> stack -> Prop :=
  | exec_nil : forall s, exec nil s s
  | exec_push : forall n s s', 
      s' = stack (n :: s.(l)) ->
      exec (IPush n :: p) s s'
  | exec_add : forall n1 n2 s s',
      s = stack (n2 :: n1 :: s'.(l)) ->
      s' = stack (n1 + n2 :: s'.(l)) ->
      exec (IAdd :: p) s s'.

Lemma compile_correct : forall e s,
  exec (compile e) s (stack (eval e :: s.(l))).
Proof.
  induction e; intros; simpl.
  - (* EConst *) constructor. simpl. constructor.
  - (* EPlus *)
    rewrite IHe1, IHe2.
    constructor. reflexivity.
    constructor. reflexivity.
    constructor.
  - (* EVar *) constructor. reflexivity.
Qed.

(* Automation *)
Hint Resolve bst_node bst_empty.
Hint Constructors bst exec.

(* CustomLtac *)
Ltac solve_by_ :=
  match goal with
  | [ H : ?P -> ?Q -> ?R |- ?R ] =>
    let H' := fresh in
    assert (H' : P); [|assert H0 : Q; [|exact (H H' H0)]]
  end.

(* Induction on complex structure *)
Lemma foo : forall l, P l.
Proof.
  induction l as [| x xs IHxs ].
  - (* nil *) ...
  - (* cons *) ...
    (* Use IH on subterm *)
    apply IHxs.
    (* Or generalize before induction *)
    generalize dependent l.
    induction x; ...
Qed.

(* Structuring large proofs *)
Section MySection.
  Variable A : Type.
  
  Lemma lemma1 : P A.
  Proof. ... Qed.
  
  Lemma lemma2 : Q A.
  Proof. ... using lemma1. ...
End MySection.