Prove the tree holds a sorted set

README.md

@@ -653,12 +653,38 @@ A lemma is a law about the code: it is tested, and it must be proved, or
 the check fails. Once proved, the spec's laws may cite it. It is reported
 apart, it counts toward no law of the spec, and the adequacy check never
 judges a stand-in by it, so a lemma can't make a weak spec look strong.
+A lemma may be about clojure.core alone, such as what a bound on a list
+says about a `filter` of it.
+
+A proof namespace may define helpers for its lemmas with `defn`, such as
+an invariant the code keeps. The prover reads them as it reads the
+target's, and a helper that refers to the target's fns reads those of
+the target under check.
+
+A lemma's hypothesis may name a variable its conclusion doesn't. The
+prover finds that variable's value in the facts of the goal at hand, the
+way ACL2 does:
+
+```clojure
+(lemma none-below
+  (forall [x Nat, v Nat, xs (List Nat)]
+    (=> (and (every? #(> % v) xs) (<= x v)) (= (filter #(< % x) xs) ()))))
+```
+
+rewrites `(filter #(< % x) r)` to `()` wherever the facts say every
+element of `r` is above some `v` with `x <= v`.
 
 A hint steers the search and nothing more: `:induct` the variable to try
-induction on first, `:use` the only lemmas and laws a proof may cite,
-`:strategy` one of `:symbolic`, `:induction` or `:rewriting`, and `:fuel`
-the rewrites one attempt may make. A proof a hint leads to is checked
-like any other.
+induction on first, `:vary` the other variables the induction hypothesis
+holds at every value of (an accumulator a fold passes on), `:use` the
+only lemmas and laws a proof may cite, `:strategy` one of `:symbolic`,
+`:induction` or `:rewriting`, and `:fuel` the rewrites one attempt may
+make. A proof a hint leads to is checked like any other.
+
+`writ.spec-demo.tree-proof` in the tests proves the tree's
+`holds-a-sorted-set` this way: a `bst?` invariant, lemmas that `insert`
+keeps it and that listing the tree after an insert is inserting into the
+list, and a fold lemma with the tree varying.
 
 ### Proofs
 
@@ -688,14 +714,32 @@ When a case still isn't closed, the prover tries two things:
   replaces the recursive call that brings in with a fresh variable, and
   proves that more general goal by an induction of its own.
   `permutation` is proved this way, with `(isort xs-t)` generalised.
+- **Sorting.** On a list of integers, `(sort xs)` and
+  `(sort (distinct xs))` are a fold that inserts each element into the
+  sorted list so far: the elements below it, it, the elements above it
+  (at or above, when duplicates stay). `writ.prove.rewrite/model-check`
+  runs the model against `sort` itself.
 - **An accumulator.** A fold that grows an accumulator by addition from
   0, as a `loop` or a `reduce`, is first proved to give acc plus the fold
   from 0, from any integer acc, by induction with acc left free in the
   hypothesis. The law is then proved citing that.
 
 A law proved earlier is a lemma for the laws after it: an equality
 rewrites its left side to its right, anything else rewrites to true, when
-its hypotheses hold. The passes repeat until nothing new is proved, so a
+its hypotheses hold.
+
+A lemma holds only at its own types, and the prover's logic is untyped,
+as ACL2's is, so a type is a hypothesis like any other. Each term a
+lemma's variable takes must be shown to be of the variable's type: a
+variable of that type is; an integer term is an Int, and a Nat when it
+can't be negative; anything else must satisfy the type's recognizer,
+which the prover builds from the spec's `data` and takes values apart
+with the way the type's cases do. A signature is only a claim, so before
+the laws, the prover proves each signed fn's contract from its code, as
+ACL2s's `defunc` does: given arguments of its parameter types, it returns
+a value of its return type. Then `(insert x t)` is known to be a `Tree`.
+A set, a map or a fn has no recognizer, and takes only a variable of its
+own type. Contracts for `Nat` and `Int` returns aren't proved yet. The passes repeat until nothing new is proved, so a
 law may cite one that comes later in the spec. A law that is only tested
 is never cited. The report names what each proof used:
 

skills/writ/SKILL.md

@@ -156,9 +156,14 @@ When a law holds but isn't proved, add what the prover needs in
 - A lemma must hold and be proved, or the check fails; it then helps
   prove the spec's laws. It never counts as one of them, and never
   judges a stand-in, so it can't strengthen a weak spec.
-- A hint: `:induct` a variable first, `:use` only these lemmas and laws,
-  `:strategy` `:symbolic` / `:induction` / `:rewriting`, `:fuel` more
-  rewrites. It only steers the search.
+- A lemma may be about clojure.core alone, and its hypothesis may name a
+  variable its conclusion doesn't: the prover takes it from the goal's
+  facts. `defn` helpers (an invariant such as `bst?`) may live in the
+  proof namespace too.
+- A hint: `:induct` a variable first, `:vary [acc]` to let the induction
+  hypothesis hold at any acc (a fold's accumulator), `:use` only these
+  lemmas and laws, `:strategy` `:symbolic` / `:induction` / `:rewriting`,
+  `:fuel` more rewrites. It only steers the search.
 - The usual reasons a law isn't proved: recursion that needs a lemma about
   a helper (write the lemma), a law about a recursive fn stated over its
   whole output where a pointwise statement would do, or a form outside

src/writ/prove.clj

@@ -12,8 +12,13 @@
 
   A proof holds for every input on which the law's terms return, as with
   Typed Clojure; writ still runs every law, which catches the inputs where
-  a term throws.  A proof that never unfolds one of the target's own
-  definitions says nothing about the code, and is not reported."
+  a term throws.  The logic is untyped, as ACL2's is: a lemma, or a
+  hypothesis that varies, is used only at terms shown to be of its
+  variables' types -- by a recognizer, and by each signed fn's contract,
+  proved from its code before any law.  A proof that never unfolds one of the target's own
+  definitions says nothing about the code, and is not reported -- unless
+  it proves a lemma of a proof namespace, which may be about clojure.core
+  alone."
   (:require [clojure.string :as str]
             [clojure.test.check.generators :as gen]
             [writ.prove.term :as t :refer [head]]
@@ -233,15 +238,27 @@
             :when p]
         {:by :generalizing :ih i :call call :as ys :ty ty :on (t/show call) :proof p}))))
 
+(defn- varying
+  "The variables of opts' :vary, but v, with their types: they stay free
+  in an induction hypothesis on v."
+  [opts v]
+  (into {} (for [x (:vary opts)
+                 :let [ty (get-in opts [:types x])]
+                 :when (and ty (not= x v))]
+             [x ty])))
+
 (defn- by-induction [opts g v ty]
   (when-let [cs (cases v ty (:tenv opts))]
-    (let [steps (for [c cs]
+    (let [free (varying opts v)
+          opts (cond-> opts (seq free) (assoc :ih-free free))
+          steps (for [c cs]
                   (let [[opts* gi] (sc/induction-case opts g v c)]
                     [c (or (prove-all opts* gi)
                            (by-generalizing (dissoc opts* :ih-free) gi (keys (:types c))))]))]
       (when (every? (comp some? second) steps)
-        {:by :induction :on v :ty (plain ty)
-         :cases (mapv (fn [[c p]] {:case (:desc c) :proof p}) steps)}))))
+        (cond-> {:by :induction :on v :ty (plain ty)
+                 :cases (mapv (fn [[c p]] {:case (:desc c) :proof p}) steps)}
+          (seq free) (assoc :vary free))))))
 
 (defn- fuelled
   "f's result, or nil when it runs out of fuel."
@@ -410,27 +427,42 @@
       (swap! (:unfolded opts) into (mapcat second rs))
       {:by :symbolic :certificates (mapv first rs)})))
 
+(defn- types-of
+  "The types a law's variables, its lemmas' and the signatures name."
+  [bs lemmas sigs]
+  (distinct (map plain (concat (map second bs)
+                               (mapcat #(map second (first (split-foralls (:prop %)))) lemmas)
+                               (mapcat (fn [[_ {:keys [params ret]}]] (cons ret params)) sigs)))))
+
+(defn- contract? [nm] (str/ends-with? (name nm) "%contract"))
+
 (defn prove-law
   "Try to prove a law.  prop is the desugared law, its names qualified;
   defs are the translated definitions; target the implementation's ns;
-  lemmas are the laws proved before it, as {:name :prop}.
+  lemmas are the laws proved before it, as {:name :prop}; lemma, true
+  for a lemma of a proof namespace, which may be about clojure.core alone;
+  sigs, the target's signatures, {name {:params :ret}}; contracts, the
+  rules prove-contracts gave for them.
   Returns {:proved true :trace :summary :lemmas} or {:proved false :reason}."
-  [{:keys [prop defs tenv target own fuel lemmas rets total hint]}]
+  [{:keys [prop defs tenv target own fuel lemmas rets total hint lemma sigs contracts]}]
   (try
     (let [[bs0 body] (split-foralls prop)
           tctx (tr/context own)
           g0 (goal tctx (mapv first bs0) body)
           [bs g] (expand-tuples (map (fn [[x ty]] [x (plain ty)]) bs0) g0)
           unfolded (atom #{})
           lemmas-used (atom #{})
+          recs (sc/recognizers tenv (types-of bs lemmas sigs))
+          defs (merge defs (:defs recs))
           opts {:defs defs :tenv tenv :types (into {} (map (fn [[x ty]] [x (plain ty)])) bs)
-                :total total
+                :total total :vary (:vary hint) :recognizers recs
                 :unfolded unfolded :fuel (or fuel 20000) :lemmas-used lemmas-used
                 :rets (or rets {})
-                :lemmas (vec (mapcat #(lemma-rules % defs tenv own)
-                                     (if-let [use (:use hint)]
-                                       (filter #(contains? (set use) (:name %)) lemmas)
-                                       lemmas)))}
+                :lemmas (into (vec (mapcat #(lemma-rules % defs tenv own)
+                                           (if-let [use (:use hint)]
+                                             (filter #(contains? (set use) (:name %)) lemmas)
+                                             lemmas)))
+                              contracts)}
           ;; an attempt that runs out of fuel fails on its own; the others
           ;; still get their turn
           ran-out (atom false)
@@ -478,16 +510,16 @@
                              [nil #{}]))
           target-used (filter #(= (str target) (namespace %)) used)
           ;; every proof is replayed by the checker before it is reported
-          checked (when (and trace (seq target-used))
+          checked (when (and trace (or lemma (seq target-used)))
                     (check/check-proof (dissoc opts :lemmas-used :unfolded) g trace))]
       (cond
         (nil? trace) (cond-> {:proved false :reason (if @ran-out "the search ran out of fuel" "no proof found")}
                        (seq bs) (merge (when-let [cex (first (keep #(sym/counterexample opts (:hyps g) %) (:goals g)))]
                                          {:counterexample (recompose bs0 cex)})))
-        (empty? target-used) {:proved false :reason "the proof does not use the code"}
+        (and (empty? target-used) (not lemma)) {:proved false :reason "the proof does not use the code"}
         (not (:ok checked)) {:proved false
                              :reason (str "the proof checker rejected the proof: " (:reason checked))}
-        :else (let [cited (sort (remove synthetic-lemmas @lemmas-used))]
+        :else (let [cited (sort (remove #(or (contains? synthetic-lemmas %) (contract? %)) @lemmas-used))]
                 {:proved true :trace trace
                  :summary (str (summary trace)
                                (when total ", and it never throws")
@@ -499,15 +531,61 @@
         (:writ.prove.rewrite/fuel (ex-data e)) {:proved false :reason "the search ran out of fuel"}
         :else (throw e)))))
 
+(defn prove-contracts
+  "Prove each signed fn's contract, as defunc does: on arguments of its
+  parameter types, it returns a value of its return type -- where that
+  type has a recognizer to say so.  A signature is only a claim; a
+  contract proved from the code is a fact, and a lemma's variable may take
+  a call of the fn as its value once the contract says the call is of the
+  variable's type.  Passes repeat while one proves something new, so a fn
+  may lean on the contracts of the fns it calls.  Each proof is replayed
+  by the checker.  Returns the proved contracts as lemma rules."
+  [{:keys [defs tenv sigs fuel]}]
+  (let [recs (sc/recognizers tenv (types-of [] [] sigs))
+        defs (merge defs (:defs recs))
+        goals (into {}
+                    (for [[f {:keys [params ret]}] (sort-by key sigs)
+                          :let [d (get defs f)
+                                c (get-in recs [:checks (plain ret)])]
+                          :when (and (:params d) (= (count params) (count (:params d)))
+                                     (vector? c) (= :app (head c)))
+                          :let [ps (mapv #(symbol (str "c%" %)) (range (count params)))
+                                types (zipmap ps (map plain params))
+                                call (into [:app f] ps)]]
+                      [f {:types types :ps ps
+                          :g {:hyps [] :goals [(t/subst c {'%x call})]}
+                          :rule {:name (symbol (str (name f) "%contract"))
+                                 :vars (set (map #(symbol (str "?" %)) ps))
+                                 :types (into {} (map (fn [p] [(symbol (str "?" p)) (types p)])) ps)
+                                 :lhs (t/subst c {'%x (into [:app f] (map #(symbol (str "?" %)) ps))})
+                                 :rhs [:lit true]}}]))
+        attempt (fn [rules {:keys [types ps g]}]
+                  (let [opts {:defs defs :tenv tenv :types types :recognizers recs
+                              :unfolded (atom #{}) :lemmas-used (atom #{}) :fuel (or fuel 20000)
+                              :lemmas rules :rets {}}
+                        trace (fuelled
+                                #(or (some->> (prove-all opts g) (hash-map :by :cases :proofs))
+                                     (first (keep (fn [p] (by-induction opts g p (types p))) ps))))]
+                    (when (and trace (:ok (check/check-proof (dissoc opts :lemmas-used :unfolded) g trace)))
+                      trace)))]
+    (loop [rules [] todo goals]
+      (let [done (into {} (keep (fn [[f x]] (when (attempt rules x) [f (:rule x)]))) todo)]
+        (if (empty? done)
+          rules
+          (recur (into rules (vals done)) (apply dissoc todo (keys done))))))))
+
 (defn definitions
   "Translate the defns of the target and the spec: [defs own].  pairs is
-  [[ns-sym forms] ...]; each ns reads its own plain names first."
+  [[ns-sym forms] ...] or [[ns-sym forms refers] ...]; each ns reads its
+  own plain names first, then the plain names in refers, name ->
+  qualified name."
   [pairs]
-  (let [qualified (into {} (for [[k v] (tr/own-names pairs) :when (namespace k)] [k v]))
+  (let [qualified (into {} (for [[k v] (tr/own-names (map #(take 2 %) pairs)) :when (namespace k)] [k v]))
         defs (into {}
-                   (for [[ns-sym forms] pairs]
-                     (let [own (merge qualified (into {} (for [[k v] (tr/own-names [[ns-sym forms]])
-                                                               :when (nil? (namespace k))]
-                                                           [k v])))]
+                   (for [[ns-sym forms refers] pairs]
+                     (let [own (merge qualified refers
+                                      (into {} (for [[k v] (tr/own-names [[ns-sym forms]])
+                                                     :when (nil? (namespace k))]
+                                                 [k v])))]
                        (tr/defs-of (tr/context own) ns-sym forms))))]
     [defs qualified]))

src/writ/prove/check.clj

@@ -107,10 +107,16 @@
       (reject! "an induction case cannot be proved " (pr-str (:by p))))))
 
 (defn- check-induction
-  "Replay an induction on v: its cases must be the type's cases."
-  [opts g {:keys [on ty cases]}]
+  "Replay an induction on v: its cases must be the type's cases.  A
+  variable that varies in the hypothesis must be one of the goal's, at its
+  own type."
+  [opts g {:keys [on ty cases vary]}]
   (let [cs (or (sc/cases on ty (:tenv opts)) (reject! "`" on "` is not of an inductive type"))
-        declared (get-in opts [:types on])]
+        declared (get-in opts [:types on])
+        _ (doseq [[x xty] vary]
+            (when (or (= x on) (not= xty (get-in opts [:types x])))
+              (reject! "`" x "` cannot vary in the hypothesis of an induction on `" on "`")))
+        opts (cond-> opts (seq vary) (assoc :ih-free vary))]
     (when-not (= (sc/plain declared) ty)
       (reject! "induction on `" on "` as " (pr-str ty) " but it is " (pr-str declared)))
     (when-not (= (map :desc cs) (map :case cases))