lib/coq/set/FsetInduction.v

   1 (********************************************************************)
   2 (*                                                                  *)
   3 (*  The Why3 Verification Platform   /   The Why3 Development Team  *)
   4 (*  Copyright 2010-2023 --  Inria - CNRS - Paris-Saclay University  *)
   5 (*                                                                  *)
   6 (*  This software is distributed under the terms of the GNU Lesser  *)
   7 (*  General Public License version 2.1, with the special exception  *)
   8 (*  on linking described in file LICENSE.                           *)
   9 (*                                                                  *)
  10 (********************************************************************)
  11
  12 (* This file is generated by Why3's Coq-realize driver *)
  13 (* Beware! Only edit allowed sections below    *)
  14 Require Import BuiltIn.
  15 Require BuiltIn.
  16 Require HighOrd.
  17 Require int.Int.
  18 Require set.Fset.
  19
  20 (* Why3 goal *)
  21 Definition t : Type.
  22 Proof.
  23 (* Example bool *)
  24 apply bool.
  25 Defined.
  26
  27 (* Why3 goal *)
  28 Definition p : set.Fset.fset t -> Prop.
  29 Proof.
  30 intros f.
  31 apply True.
  32 Defined.
  33
  34 (* Why3 goal *)
  35 Lemma Induction :
  36   (forall (s:set.Fset.fset t), set.Fset.is_empty s -> p s) ->
  37   (forall (s:set.Fset.fset t), p s -> (forall (t1:t), p (set.Fset.add t1 s))) ->
  38   forall (s:set.Fset.fset t), p s.
  39 Proof.
  40 intros h1 h2 s.
  41 (* TODO make something interesting *)
  42 unfold p. constructor.
  43 Qed.
  44