IV. Logic and proofs

3. We define two transformations rules to:

b. apply an hypothesis

let apply h (hs,p::ps) = 
 let v = List.filter (fun (k,r)->k=h) hs
 match v with
 | []       -> (hs,p::ps)
 | (_,q)::_ -> if p=q then (hs,ps) else (hs,p::ps);;

let s3 = apply "h1" s2;; // = ???

"Application" is easy to understand: if a proposition to demonstrate is already present in the hypothesis (:what is admitted) then the proof is complete for that proposition.

4 - 12