coq_induction_principle_generation.v

Section __.
  Context (A : Type).
  Inductive list := cons (_:A) (_:list) | nil.
  Check list_ind : forall P : _ -> Prop,
      (forall a l, P l -> P (cons a l)) ->
      P nil ->
      forall l : list, P l.

  Inductive btree := branch (_:A) (_:btree) (_:btree) | leaf.
  Check btree_ind : forall P : btree -> Prop,
       (forall a t1, P t1 -> forall t2, P t2 -> P (branch a t1 t2)) ->
       P leaf ->
       forall b : btree, P b.

  Inductive ntree := fanout (_:A) (_:Datatypes.list ntree) | nleaf.
  Check ntree_ind : forall P : ntree -> Prop,
      (forall a l, P (fanout a l)) -> (* <-- missing IH *)
      P nleaf ->
      forall n : ntree, P n.

  Inductive ntree_hack := hfanout (_:A) (_:ntree_list) | hleaf
  with ntree_list := ntree_cons (_:A) (_:ntree_list) | ntree_nil.
  Check ntree_hack_ind : forall P : ntree_hack -> Prop,
      (forall a l, P (hfanout a l)) -> (* <-- missing IH *)
      P hleaf ->
      forall n : ntree_hack, P n.

  (* the automatically generated eliminators are wrong, but we can ask for better ones using the following incantation *)

  Scheme ntree_hack_ind_correct := Induction for ntree_hack Sort Prop
    with ntree_list_ind_correct := Induction for ntree_list Sort Prop.
  Combined Scheme ntree_hack_ntree_list_mutind
           from ntree_hack_ind_correct, ntree_list_ind_correct.
  Check ntree_hack_ntree_list_mutind : forall (P : ntree_hack -> Prop) (Q : ntree_list -> Prop),
       (forall (a : A) (n : ntree_list), Q n -> P (hfanout a n)) ->
       P hleaf ->

       (forall (a : A) (n : ntree_list), Q n -> Q (ntree_cons a n)) ->
       Q ntree_nil ->
       
       (forall n : ntree_hack, P n) /\ (forall n : ntree_list, Q n).
End __.

Module collatz.
  Inductive collatz : nat -> Prop :=
  | collatz1 : collatz 1
  | collatz_rec_even n
    (_ : Nat.even n = true)
    (_ : collatz (Nat.div n 2))
    : collatz n
  | collatz_rec_odd n
    (_ : Nat.even n = false)
    (_ : collatz (3*n+1))
    : collatz n
  .
  Check collatz_ind : forall P : nat -> Prop,
       P 1 ->
       (forall n, Nat.even n = true  -> collatz (Nat.div n 2) -> P (Nat.div n 2) -> P n) ->
       (forall n, Nat.even n = false -> collatz (3 * n + 1  ) -> P (3 * n + 1)   -> P n) ->
       forall n : nat, collatz n -> P n.
End collatz.

Module collatz_nested.
  Inductive collatz : nat -> Prop :=
  | collatz1 : collatz 1
  | collatz_rec n
                (_ : or
                       (and (Nat.even n = true ) (collatz (Nat.div n 2)))
                       (and (Nat.even n = false) (collatz (3*n+1))))
    : collatz n
  .
  Check collatz_ind : forall P : nat -> Prop,
       P 1 ->
       (forall n,
           or (and (Nat.even n = true ) (collatz (Nat.div n 2)))
              (and (Nat.even n = false) (collatz (3*n+1)))
              (* missing IH *)
           -> P n) ->
       forall n : nat, collatz n -> P n.
End collatz_nested.

Module collatz_mutual.
  Fail Inductive collatz : nat -> Prop :=
  | collatz1 : collatz 1
  | collatz_rec n
                (_ : or (and (Nat.even n = true ) (collatz (Nat.div n 2)))
                        (and (Nat.even n = false) (collatz (3*n+1))))
    : collatz n
  with
  and : forall (A B : Prop), Prop :=  conj (A B:Prop) (_ : A) (_ : B) : and A B
  with
  or : forall (A B : Prop), Prop := or_introl (A B:Prop) (_ : A) : or A B | or_intror (A B : Prop) (_:B) : or A B
  .
  (*
The command has indeed failed with message:
Non strictly positive occurrence of "and" in
 "forall n : nat,
  or (and (Nat.even n = true) (collatz (Nat.div n 2)))
    (and (Nat.even n = false) (collatz (3 * n + 1))) -> collatz n".
*)
  Fail Inductive collatz : nat -> Prop :=
  | collatz1 : collatz 1
  | collatz_rec n
                (_ : and (Nat.even n = true  -> collatz (Nat.div n 2))
                         (Nat.even n = false -> collatz (3*n+1)))
    : collatz n
  with
  and : forall (A B : Prop), Prop :=  conj (A B:Prop) (_ : A) (_ : B) : and A B
  .
(*
Non strictly positive occurrence of "collatz" in
 "forall n : nat,
  and (Nat.even n = true -> collatz (Nat.div n 2))
    (Nat.even n = false -> collatz (3 * n + 1)) -> collatz n".
*)
End collatz_mutual.

Module collatz_under_if.
  Fail Inductive collatz : nat -> Prop :=
  | collatz1 : collatz 1
  | collatz_rec_even n
    (_ : if Nat.even n then collatz (Nat.div n 2) else collatz (3*n+1))
    : collatz n.
  (* Non strictly positive occurrence of "collatz" in
 "forall n : nat,
  (if Nat.even n then collatz (Nat.div n 2) else collatz (3 * n + 1)) -> collatz n". *)
End collatz_under_if.

Module collatz_if_in_inductive_occurrance_arument.
  Inductive collatz : nat -> Prop :=
  | collatz1 : collatz 1
  | collatz_rec_even n
    (_ : collatz (if Nat.even n then (Nat.div n 2) else (3*n+1)))
    : collatz n.
  Check collatz_ind : forall P : nat -> Prop,
       P 1 ->
       (forall n, collatz (if Nat.even n then Nat.div n 2 else 3 * n + 1) ->
                  P (if Nat.even n then Nat.div n 2 else 3 * n + 1)       -> P n)
       -> forall n : nat, collatz n -> P n.
End collatz_if_in_inductive_occurrance_arument.

Module collatz_under_forall.
  Inductive collatz : nat -> Prop :=
  | collatz1 : collatz 1
  | collatz_rec_even n
    (_ : forall
           (next : nat)
           (_ : next = if Nat.even n then Nat.div n 2 else 3*n+1),
           collatz next)
    : collatz n.
  Check collatz_ind : forall P : nat -> Prop,
    P 1 ->
    (forall n,
       (forall next : nat, next = (if Nat.even n then Nat.div n 2 else 3 * n + 1) -> collatz next) ->
       (forall next : nat, next = (if Nat.even n then Nat.div n 2 else 3 * n + 1) -> P next)       -> P n) ->
    forall n : nat, collatz n -> P n.
End collatz_under_forall.

(* even more complicated example of encoding away [and] and [or], from https://github.com/mit-plv/bedrock2/blob/f7a62aea6dd89a71b9ba23c9195e90bd20210665/compiler/src/FlatToRiscv.v#L1884 *)

(*
  Inductive exec:
    stmt ->
    trace -> @Memory.mem mword -> locals ->
    (trace -> @Memory.mem mword -> locals -> Prop)
    -> Prop :=
  | ExInteract: forall t m l action argvars argvals resvars outcome post,
      option_all (List.map (get l) argvars) = Some argvals ->
      ext_spec action argvals outcome ->
      (forall newEvents resvals,
          outcome newEvents resvals ->
          exists l', putmany resvars resvals l = Some l' /\ post (newEvents ++ t) m l') ->
      exec (SInteract resvars action argvars) t m l post
  | ExLoad: forall t m l x a v addr post,
      get l a = Some addr ->
      Memory.read_mem addr m = Some v ->
      post t m (put l x v) ->
      exec (SLoad x a) t m l post
(* ... *)
  | ExIfThen: forall t m l cond vcond bThen bElse post,
      get l cond = Some vcond ->
      vcond <> ZToReg 0 ->
      exec bThen t m l post ->
      exec (SIf cond bThen bElse) t m l post
  | ExIfElse: forall t m l cond bThen bElse post,
      get l cond = Some (ZToReg 0) ->
      exec bElse t m l post ->
      exec (SIf cond bThen bElse) t m l post
  | ExLoop: forall t m l cond body1 body2 mid post,
      (* this case is carefully crafted in such a way that recursive uses of exec
         only appear under forall and ->, but not under exists, /\, \/, to make sure the
         auto-generated induction principle contains an IH for both recursive uses *)
      exec body1 t m l mid ->
      (forall t' m' l', mid t' m' l' -> get l' cond <> None) ->
      (forall t' m' l',
          mid t' m' l' ->
          get l' cond = Some (ZToReg 0) -> post t' m' l') ->
      (forall t' m' l',
          mid t' m' l' ->
          forall v,
            get l' cond = Some v ->
            v <> ZToReg 0 ->
            exec (SSeq body2 (SLoop body1 cond body2)) t' m' l' post) ->
      exec (SLoop body1 cond body2) t m l post
*)