úÎ\¸X†$      !"# Safe-Inferred$#Concatenate the results after mapM %Function composition deluxe  (f .: g) = x y -> f (g x y)& O(n log n) group, but destroys ordering ' O(n log n)1 nub by a comparison function. Destroys ordering $%&'$%&'$%&' Safe-Inferred'Obligations with tagged variables (see  and ) .Cheap way of introducing fresh variables. The ( and ) instances  only uses the * tag. DGiven a type, return either that you cannot do induction on is type  (+), or ,7 the constructors and a description of their arguments  (see ).  The function !should instantiate type variables. For instance, if you look  up the type [Nat]8, you should return the cons constructor with arguments  Nat and [Nat] (see ). JExamples of types not possible to do induction on are function spaces and # type variables. For these, return +. /An argument to a constructor can be recursive ( ) or non-recursive  (.). Induction hypotheses will be asserted for   arguments. &For instance, when doing induction on [a], then (:) has two arguments,  NonRec a and Rec [a]+. On the other hand, if doing induction on [Nat],  then (:) has  NonRec Nat and Rec [Nat]. -Data types can also be exponential. Consider  -data Ord = Zero | Succ Ord | Lim (Nat -> Ord) Here, the Lim6 constructor is exponential. If we describe types and D constructors with strings, the constructors for this data type is:  [ ("Zero",[]) , ("Succ",[Rec "Ord"]) &, ("Lim",[Exp ("Nat -> Ord") ["Nat"]) ] The first argument to - is the type of the function, and the second - argument are the arguments to the function. HQuantifier lists are represented as tuples of variables and their type.  Example:  ([(x,t1),(y,t2)] ,[tm1,tm2])corresponds to the formula %forall (x : t1) (y : t2) . P(tm1,tm2) HQuantifier lists are represented as tuples of variables and their type.  Example:   Obligation # { implicit = [(x,t1),(y,t2)] % , hypotheses = [([],[htm1,htm2]) + ,([(z,t3)],[htm3,htm4])  ]  , conclusion = [tm1,tm2]  } Corresponds to the formula: Zforall (x : t1) (y : t2) . (P(htm1,htm2) & (forall (z : t3) . P(htm3,htm4)) => P(tm1,tm2)) The implicit variables (x and y') can be viewed as skolemised, and use  these three formulae instead:  P(htm1,htm2). forall (z : t3) . P(htm3,htm4).  ~ P(tm1,tm2). -Implicitly quantified variables (skolemised) 1Hypotheses, with explicitly quantified variables The induction conclusion A list of terms.  Example: [tm1,tm2] corresponds to the formula  P(tm1,tm2) NThe simple term language only includes variables, constructors and functions. EInduction on exponential data types yield assumptions with functions The * tag .Removing tagged (fresh) variables in a monad. $ The remove function is exectued at every occurence of a tagged variable. H This is useful if you want to sync it with your own name supply monad. "Removing tagged (fresh) variables ,Remove tagged (fresh) variables in a monad. ! The remove function is exectued  only once for each tagged variable,  and a - of renamings is returned. H This is useful if you want to sync it with your own name supply monad.  ./    ./ Safe-Inferred(Functions for linearising constructors (), variables () and  types (). LAn example style where constructors, variables and types are represented as 0. Linearises a list of  , using a given . Linearises an   using a given . The output format is / inspired by TPTP, but with typed quantifiers. ! Linearises a  using a given .  !1234567  !  !1234567None 8A monad of fresh Integers 9Tagged hypotheses : Tagged terms ;'Get the representation of the argument <Run the fresh monad =Creating a fresh variable >(Create a fresh variable that has a type ?Refresh variable @#Refresh a variable that has a type 8A9:;<=>?@ 8A9:;<=>?@ 8A9:;<=>?@NoneBBFind the type of a variable using the index in a type environment CJInstantiate a variable with a given type, returning the new variables and ) what the term should be replaced with D&Induction on every variable in a term 8Assumption: The variables only occur once in each term. E&Induction several times on a variable F9Unroll to a given depth, but does not add any hypotheses GDMake Obligations: this means to add empty hypotheses to QuantTerms. H<Removes the argument type information from the constructors IHRemoves the argument type information from the constructors in one Term "IDoes case analysis on a list of typed variables. This function is equal % to removing all the hypotheses from #. J<Gets all well-typed subterms of a term, including yourself. 'The first argument is always yourself. JWe need terms where the constructors are associated with their arguments. K-Does this term contain a variable somewhere? L"Adds hypotheses to an Obligation. FImportant to drop 1, otherwise we get the conclusion as a hypothesis! FHypotheses that only contain constructors (no variables) are removed. MEAdds hypotheses to an Obligation, requantifying over naked variables #I.e. forall x y . P(K x,y) becomes  forall x y . (forall y'.P(x,y')) -> P (K x,y) FImportant to drop 1, otherwise we get the conclusion as a hypothesis! #DSubterm induction: the induction hypotheses will contain the proper  subterms of the conclusion. NOPBQCDEFGHI"JKLM#"#NOPBQCDEFGHI"JKLM#None$  !"#$#"    !R      !!"#$%&'()*+,-./01/02345678679:;<=>6?@ABCDEFGHIJKLMNOPHQRSTUVWXYZ[\]^_`astructural-induction-0.1Induction.StructuralInduction.Structural.AuxiliaryInduction.Structural.TypesInduction.Structural.LineariseInduction.Structural.UtilsInduction.Structural.Subtermspretty-1.1.1.0Text.PrettyPrint.HughesPJrendertextTaggedObligationTagged:~TyEnvArgExpNonRecRec Hypothesis Obligationimplicit hypotheses conclusion PredicateTermFunConVartagunTagMunTag unTagMapMStylelinclinvlintstrStylelinObligations linObligationlinTerm caseAnalysissubtermInduction concatMapM.: groupSortedOn nubSortedOnghc-prim GHC.ClassesEqOrd integer-gmpGHC.Integer.TypeIntegerbase Data.MaybeNothingJustcontainers-0.5.0.0 Data.Map.BaseMap $fOrdTagged $fEqTaggedGHC.BaseStringcsvparList ampersandbangfluffdarrowdotFreshTaggedHypothesis TaggedTermargReprrunFreshnewFreshnewTyped refreshTaggedrefreshTypedTagged mfindVNoteinst inductionTmrepeatInductionTmnoHypsmakeObligations removeArgs removeArgsubtermshasVar addHypothesesaddHypothesesQ QuantTerms QuantTermCmakeQuantTerms