Functional Programming & Proofs
IV. Logic and proofs
- 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
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide