Examples of usages of second order theorems (induction invariants and friends)

Classes of Second order theorems

• Induction principles
• Loop invariants/VST etc.
• Comparison functions?
• Logical Relations

Examples from Coq code in Github

Acc_ind

Note: Does not fully reduce; may need dataflow analysis.

nat_ind

Require Import Arith.

Lemma add_comm :
  forall a b,
    a + b = b + a.
Proof.
  intros a.
  pose (fun b => a + b = b + a) as I.
  (* evar (HI: I 0). *)
  (* evar (HInd: (forall n : nat, I n -> I (S n))). *)
  (* print_reduced (nat_ind I ?HI ?HInd 3). *)
  apply (nat_ind (fun b : nat => a + b = b + a)).
  rewrite <- plus_n_O.
  rewrite plus_O_n.
  reflexivity.
  intros n Hn.
  rewrite <- plus_n_Sm.
  rewrite  plus_Sn_m.
  rewrite Nat.add_comm.
  reflexivity.
Qed.

ex_ind

Variables A : Set.
Variables P Q : A -> Prop.
Lemma ex_3 : (exists x : A, P x \/ Q x) -> ex P \/ ex Q.
  intros.
  apply ex_ind with (P0 := ex P \/ ex Q) in H.
  apply H.
  intros.
  apply or_ind with (P := (ex P \/ ex Q)) in H0.
  apply H0.
  intro.
  apply or_introl.
  apply ex_intro with (x := x).
  apply H1.
  intro.
  apply or_intror.
  apply ex_intro with (x := x).
  apply H1.
Qed.

well_founded_ind

Set Implicit Arguments.
Set Strict Implicit.

Section PairWF.
  Variables T U : Type.
  Variable RT : T -> T -> Prop.
  Variable RU : U -> U -> Prop.

  Inductive R_pair : T * U -> T * U -> Prop :=
  | L : forall l l' r r',
    RT l l' -> R_pair (l,r) (l',r')
  | R : forall l r r',
    RU r r' -> R_pair (l,r) (l,r').

  Hypothesis wf_RT : well_founded RT.
  Hypothesis wf_RU : well_founded RU.

  Theorem wf_R_pair : well_founded R_pair.
  Proof.
    red. intro x.
    destruct x. generalize dependent u.
    apply (well_founded_ind wf_RT (fun t => forall u : U, Acc R_pair (t, u))) .
    do 2 intro.

    apply (well_founded_ind wf_RU (fun u => Acc R_pair (x,u))). intros.
    constructor. destruct y.
    remember (t0,u). remember (x,x0). inversion 1; subst;
    inversion H4; inversion H3; clear H4 H3; subst; eauto.
  Defined.
End PairWF.

Require Export Arith.
Require Export ArithRing.
Require Export Wf_nat.

Section div_it_assumed.

Parameter div_it : forall (n m : nat), 0 < m ->  nat * nat.

Hypothesis
   div_it_fix_eqn :
   forall (n m : nat) (h : 0 < m),
    div_it n m h = match le_gt_dec m n with
                     left H => let (q, r) := div_it (n - m) m h in (S q, r)
                    | right H => (0, n)
                   end.

Theorem div_it_correct1:
 forall (m n : nat) (h : 0 < n),
  m = fst (div_it m n h) * n + snd (div_it m n h).
Proof.

  intros m.
  Check (well_founded_ind lt_wf).
  Check (fun m => forall (n : nat) (h : 0 < n), m = fst (div_it m n h) * n + snd (div_it m n h)).
  Check (well_founded_ind lt_wf (fun m => forall (n : nat) (h : 0 < n), m = fst (div_it m n h) * n + snd (div_it m n h))).
  apply ((well_founded_ind lt_wf (fun m => forall (n : nat) (h : 0 < n), m = fst (div_it m n h) * n + snd (div_it m n h)))).
  intros m' Hrec.
intros  n h; rewrite div_it_fix_eqn.
case (le_gt_dec n m'); intros H; trivial.
pattern m' at 1; rewrite (le_plus_minus n m'); auto.
pattern (m' - n) at 1; rewrite Hrec with (m' - n) n h; auto with arith.
case (div_it (m' - n) n h); simpl; auto with arith.
Qed.

Require Import Program Div2 Omega.
Require Import Arith Arith.Even Arith.Div2 NPeano.
Require Import Coq.Program.Wf Init.Wf.
Require Import Coq.Arith.Max.
Require Import Coq.Arith.Mult.


Fixpoint sum (i j : nat) (f : nat -> nat) : nat :=
  match (Nat.compare i j) with
  | Lt => match j with
               | 0 => 0
               | S j' => sum i j' f + f j
             end
  | Eq => f i
  | Gt => 0
  end.

Lemma sum_adds_0 :
  forall j f, sum 0 j f = f 0 + sum 1 j f.
Proof.
intros.
apply (well_founded_ind
          lt_wf
          (fun j =>  sum 0 j f = f 0 + sum 1 j f)).
intros.
destruct x. simpl. omega.
simpl.
destruct x. simpl. auto.
 rewrite plus_assoc. rewrite <- H. auto. auto.
Qed.

le_ind

Theorem n_le_m__Sn_le_Sm : forall n m,
  n <= m -> S n <= S m.
Proof.
  intros.
  induction H using le_ind.
  - apply le_n.
  - apply le_S.
    apply IHle.

    Restart.
    intros.
    Check le_ind n (fun m => S n <= S m).
    apply (le_ind n (fun m => S n <= S m)).
  - apply le_n.
  - intros.
    apply le_S.
    apply H1.
  - apply H.
Qed.

list_ind

Lemma map_compose {A B C : Type} (f : A -> B) (g : B -> C) (xs : list A) :
  map (fun x => g (f x)) xs = map g (map f xs).
Proof.
  revert xs.
  Check list_ind (fun xs =>  map (fun x : A => g (f x)) xs = map g (map f xs)).
  apply (list_ind (fun xs =>  map (fun x : A => g (f x)) xs = map g (map f xs))).
  - reflexivity.
  - intros x xs IH. rewrite !map_cons, IH. reflexivity.
Qed.

nat_double_ind

Lemma minus_le_lem2c : forall a b : nat, a - S b <= a - b.
intros. pattern a, b in |- *. apply nat_double_ind. auto with arith.
intro. elim minus_n_O. rewrite minus_n_SO. simpl in |- *. auto with arith.
intros. simpl in |- *. exact H.
Qed.

From Coq Require Export ZArith.
From Coq Require Import Lia.
Require Export Coq.Arith.Even.
Require Export Coq.Arith.Max.
Require Export Coq.Arith.Min.
Require Import Coq.Logic.Eqdep_dec.
Require Import Coq.Setoids.Setoid.

(* begin hide *)
Coercion Zpos : positive >-> Z.
Coercion Z_of_nat : nat >-> Z.
(* end hide *)

Definition caseZ_diff {A : Type} (z : Z) (f : nat -> nat -> A) :=
  match z with
  | Z0 => f 0 0
  | Zpos m => f (nat_of_P m) 0
  | Zneg m => f 0 (nat_of_P m)
  end.

Lemma caseZ_diff_Pos : forall (A : Type) (f : nat -> nat -> A) (n : nat),
  caseZ_diff n f = f n 0.
Proof.
 intros A f n.
 elim n.
  reflexivity.
 intros n0 H.
 simpl in |- *.
 rewrite nat_of_P_o_P_of_succ_nat_eq_succ.
 reflexivity.
Qed.

Lemma caseZ_diff_Neg : forall (A : Type) (f : nat -> nat -> A) (n : nat),
 caseZ_diff (- n) f = f 0 n.
Proof.
 intros A f n.
 elim n.
  reflexivity.
 intros n0 H.
 simpl in |- *.
 rewrite nat_of_P_o_P_of_succ_nat_eq_succ.
 reflexivity.
Qed.

Lemma proper_caseZ_diff : forall (A : Type) (f : nat -> nat -> A),
 (forall m n p q : nat, m + q = n + p -> f m n = f p q) ->
 forall m n : nat, caseZ_diff (m - n) f = f m n.
Proof.
 intros A F H m n.
 pattern m, n in |- *.
 Check nat_double_ind.
 apply (nat_double_ind ((fun n0 n1 : nat => caseZ_diff (n0 - n1) F = F n0 n1))).
   intro n0.
   replace (0%nat - n0)%Z with (- n0)%Z.
    rewrite caseZ_diff_Neg.
    reflexivity.
   simpl in |- *.
   reflexivity.
  intro n0.
  replace (S n0 - 0%nat)%Z with (Z_of_nat (S n0)).
   rewrite caseZ_diff_Pos.
   reflexivity.
  simpl in |- *.
  reflexivity.
 intros n0 m0 H0.
 rewrite (H (S n0) (S m0) n0 m0).
  rewrite <- H0.
  replace (S n0 - S m0)%Z with (n0 - m0)%Z.
   reflexivity.
  repeat rewrite Znat.inj_S.
  auto with zarith.
 auto with zarith.
Qed.

Theorem le_or_lt : forall n m, n <= m \/ m < n.
Proof.
  intros n m; pattern n, m; apply nat_double_ind; auto with arith.
  induction 1; auto with arith.
Qed.

Lemma mult_minus_distr_r : forall n m p, (n - m) * p = n * p - m * p.
Proof.
  intros.
  Check nat_double_ind.
  apply (nat_double_ind (fun n m => (n - m) * p = n * p - m * p)); simpl; auto with arith.
  intros. rewrite <- minus_plus_simpl_l_reverse; auto with arith.
Qed.

List.rev_ind

Require Import List.
Require Import sflib. (* Software Foundations Lib *)

Notation "[ x ]" := (cons x nil) : list_scope.

Definition lastn {A} (n: nat) (l: list A) :=
  List.rev (List.firstn n (List.rev l)).

Lemma lastn_snoc A n (l:list A) x:
  lastn (S n) (l ++ [x]) = (lastn n l) ++ [x].
Proof.
  revert n. induction l using List.rev_ind; ss.
  unfold lastn. s. rewrite List.rev_app_distr. ss.
Qed.

well_founded_induction_type

Inductive lt_nat2 : (nat * nat) -> (nat * nat) -> Prop :=
| fst_lt2 : forall a b c d, a < b -> lt_nat2 (a , c) (b, d)
| snd_lt2 : forall a b c, b < c -> lt_nat2 (a, b) (a, c).

Notation "a <2 b" := (lt_nat2 a b) (at level 90) : nat_scope.

Lemma wf_lt_nat2 : well_founded lt_nat2.
Proof.
  intros [n m].
  revert m.
  apply (lt_wf_ind n) ; clear n.
  intros n Hn m.
  apply (lt_wf_ind m); clear m.
  intros m Hm.
  apply Acc_intro.
  intros [n' m'] Hlt2.
  inversion Hlt2; subst.
  - apply Hn.
    apply H0.
  - apply Hm.
    apply H0.
Qed.

Lemma lt_nat2_wf_rect :
  forall n (P:(nat*nat) -> Type), (forall n, (forall m, m <2 n -> P m) -> P n) -> P n.
Proof.
intros n P Hw.
apply well_founded_induction_type with lt_nat2.
- apply wf_lt_nat2.
- assumption.
Qed.

N.order_induction

Lemma Z_succ_pred_induction y (P : Z → Prop) :
  P y →
  (∀ x, y ≤ x → P x → P (Z.succ x)) →
  (∀ x, x ≤ y → P x → P (Z.pred x)) →
  (∀ x, P x).
Proof. intros H0 HS HP. by apply (Z.order_induction' _ _ y). Qed.

rtclosure_ind

Require Import Setoid.
Require Export LibListSorted.
Require Export LibList.
Require Export LibFset.
Require Export LibRelation.


Notation " Ctx *=* Ctx'" := (permut Ctx Ctx') (at level 70) : permut_scope.

Variable A:Type.

Inductive Permutation : list A -> list A -> Prop :=
| perm_nil: Permutation nil nil
| perm_skip x l l' : Permutation l l' -> Permutation (x::l) (x::l')
| perm_swap x y l : Permutation (y::x::l) (x::y::l)
| perm_trans l l' l'' :
  Permutation l l' -> Permutation l' l'' -> Permutation l l''.

Local Hint Constructors Permutation.

Theorem permut_equiv:
forall l1 l2,
  l1 *=* l2 <->
  Permutation l1 l2.
split; intro.
generalize dependent l2;
generalize dependent l1;
apply rtclosure_ind; intros; auto;
transitivity y; auto; inversion H; subst; apply Permutation_swap_middle.
induction H; permut_simpl; auto; transitivity l'; auto.
Qed.

Z.left_induction

See this file with higher-order function

N.order_induction

Coercion Z.of_nat : nat >-> Z.
Local Open Scope Z_scope.

Notation "(≤)" := Z.le (only parsing) : Z_scope.

Lemma Z_succ_pred_induction y (P : Z ->  Prop) :
  P y ->
  (forall x, y <= x -> P x -> P (Z.succ x)) ->
  (forall x, x <= y -> P x -> P (Z.pred x)) ->
  (forall x, P x).
Proof. intros H0 HS HP.
       now apply (Z.order_induction' _ _ y).
Qed.

Non-Induction

well_founded_lt_compat

Definition lengthOrder {A : Type} (l1 l2 : list A) : Prop :=
  length l1 < length l2.

Theorem lengthOrder_wf : forall (A : Type),
    well_founded (@lengthOrder A).
Proof.
  unfold lengthOrder. intro.
  apply (@well_founded_lt_compat _ (@length A)). trivial.
Defined.

(* sublist wf induction *)
Inductive strictsublist {A : Type} : list A -> list A -> Prop :=
   | strictsublist_nil : forall h t, strictsublist nil (h :: t)
   | strictsublist_skip : forall l1 h t, strictsublist l1 t -> strictsublist l1 (h :: t)
   | strictsublist_cons : forall h t1 t2, strictsublist t1 t2 -> strictsublist (h :: t1) (h :: t2).

Lemma strictsublist_wf (A : Type) :
     well_founded (strictsublist (A := A)).
Proof.
     eapply well_founded_lt_compat with (f := (length (A := A))).
     intros l1 l2 H.
     induction H; simpl; auto with arith.
Qed.

le_elim_rel

Lemma minus_le_O : forall a b : nat, a <= b -> a - b = 0.
Proof.
  intros. pattern a, b in |- *.
  apply le_elim_rel. auto with arith.
intros. simpl in |- *. exact H1.
exact H.
Qed.

Lemma minus_Sn_m : forall n m, m <= n -> S (n - m) = S n - m.
Proof.
  intros n m Le; pattern m, n; apply le_elim_rel; simpl;
    auto with arith.
Qed.