diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-11-26 01:00:41 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-11-26 01:00:41 +0000 |
| commit | fa4b252945a870100305c159d20e264be18973ce (patch) | |
| tree | 435cbd07a2af45f3f08dc8ac892fa48044047eeb /docs/proof/Vericertlib.html | |
| parent | 29bee524cccfe08c680f655b1969a4c421e0a969 (diff) | |
| download | vericert-kvx-fa4b252945a870100305c159d20e264be18973ce.tar.gz vericert-kvx-fa4b252945a870100305c159d20e264be18973ce.zip | |
Add proof documentation
Diffstat (limited to 'docs/proof/Vericertlib.html')
| -rw-r--r-- | docs/proof/Vericertlib.html | 259 |
1 files changed, 259 insertions, 0 deletions
diff --git a/docs/proof/Vericertlib.html b/docs/proof/Vericertlib.html new file mode 100644 index 0000000..52dd27c --- /dev/null +++ b/docs/proof/Vericertlib.html @@ -0,0 +1,259 @@ +<?xml version="1.0" encoding="utf-8" ?> +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml" class="alectryon-standalone" xml:lang="en" lang="en"> +<head> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<meta name="generator" content="Docutils 0.16: http://docutils.sourceforge.net/" /> +<title>Vericertlib.v</title> +<link rel="stylesheet" href="alectryon.css" type="text/css" /> +<link rel="stylesheet" href="docutils_basic.css" type="text/css" /> +<link rel="stylesheet" href="tango_subtle.css" type="text/css" /> +<link rel="stylesheet" href="tango_subtle.min.css" type="text/css" /> +<script type="text/javascript" src="alectryon.js"></script> +<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/IBM-type/0.5.4/css/ibm-type.min.css" integrity="sha512-sky5cf9Ts6FY1kstGOBHSybfKqdHR41M0Ldb0BjNiv3ifltoQIsg0zIaQ+wwdwgQ0w9vKFW7Js50lxH9vqNSSw==" crossorigin="anonymous" /> +<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/firacode/5.2.0/fira_code.min.css" integrity="sha512-MbysAYimH1hH2xYzkkMHB6MqxBqfP0megxsCLknbYqHVwXTCg9IqHbk+ZP/vnhO8UEW6PaXAkKe2vQ+SWACxxA==" crossorigin="anonymous" /> +</head> +<body> +<div class="alectryon-root alectryon-floating"><div class="document"> + + +<pre class="alectryon-io"><!-- Generator: Alectryon v1.0 --><span class="coq-wsp"><span class="highlight"><span class="c">(*</span> +<span class="c"> * Vericert: Verified high-level synthesis.</span> +<span class="c"> * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com></span> +<span class="c"> *</span> +<span class="c"> * This program is free software: you can redistribute it and/or modify</span> +<span class="c"> * it under the terms of the GNU General Public License as published by</span> +<span class="c"> * the Free Software Foundation, either version 3 of the License, or</span> +<span class="c"> * (at your option) any later version.</span> +<span class="c"> *</span> +<span class="c"> * This program is distributed in the hope that it will be useful,</span> +<span class="c"> * but WITHOUT ANY WARRANTY; without even the implied warranty of</span> +<span class="c"> * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the</span> +<span class="c"> * GNU General Public License for more details.</span> +<span class="c"> *</span> +<span class="c"> * You should have received a copy of the GNU General Public License</span> +<span class="c"> * along with this program. If not, see <https://www.gnu.org/licenses/>.</span> +<span class="c"> *)</span> + +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">From</span> Coq <span class="kn">Require Export</span> + String + ZArith + Znumtheory + List + Bool.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Require Import</span> Lia.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">From</span> vericert <span class="kn">Require Import</span> <span class="kn">Show</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +<span class="c">(* Depend on CompCert for the basic library, as they declare and prove some</span> +<span class="c"> useful theorems. *)</span> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">From</span> compcert.lib <span class="kn">Require Export</span> Coqlib.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">From</span> compcert <span class="kn">Require Import</span> Integers.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Local Open Scope</span> Z_scope.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +<span class="c">(* This tactic due to Clement Pit-Claudel with some minor additions by JDP to</span> +<span class="c"> allow the result to be named: https://pit-claudel.fr/clement/MSc/#org96a1b5f *)</span> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Inductive</span> <span class="nf">Learnt</span> {<span class="nv">A</span>: <span class="kt">Type</span>} (<span class="nv">a</span>: A) := + | AlreadyKnown : Learnt a.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Ltac</span> <span class="nf">learn_tac</span> fact name := + <span class="kr">lazymatch goal with</span> + | [ H: Learnt fact |- _ ] => + <span class="kp">fail</span> <span class="mi">0</span> <span class="s2">"fact"</span> fact <span class="s2">"has already been learnt"</span> + | _ => <span class="kr">let</span> <span class="nv">type</span> := <span class="kp">type of</span> fact <span class="kr">in</span> + <span class="kr">lazymatch goal with</span> + | [ H: @Learnt type _ |- _ ] => + <span class="kp">fail</span> <span class="mi">0</span> <span class="s2">"fact"</span> fact <span class="s2">"of type"</span> type <span class="s2">"was already learnt through"</span> H + | _ => <span class="kr">let</span> <span class="nv">learnt</span> := <span class="kp">fresh</span> <span class="s2">"Learn"</span> <span class="kr">in</span> + <span class="nb">pose proof</span> (AlreadyKnown fact) <span class="kr">as</span> learnt; <span class="nb">pose proof</span> fact <span class="kr">as</span> name + <span class="kr">end</span> + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Tactic Notation</span> <span class="s2">"learn"</span> <span class="kp">constr</span>(fact) := <span class="kr">let</span> <span class="nv">name</span> := <span class="kp">fresh</span> <span class="s2">"H"</span> <span class="kr">in</span> learn_tac fact name.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Tactic Notation</span> <span class="s2">"learn"</span> <span class="kp">constr</span>(fact) <span class="s2">"as"</span> simple_intropattern(name) := learn_tac fact name.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Ltac</span> <span class="nf">unfold_rec</span> c := <span class="nb">unfold</span> c; <span class="nb">fold</span> c.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Ltac</span> <span class="nf">solve_by_inverts</span> n := + <span class="kr">match goal with</span> | H : <span class="nl">?T</span> |- _ => + <span class="kr">match</span> <span class="kp">type of</span> T <span class="kr">with</span> <span class="kt">Prop</span> => + <span class="nb">inversion</span> H; + <span class="kr">match</span> n <span class="kr">with</span> S (S (<span class="nl">?n'</span>)) => <span class="nb">subst</span>; <span class="kp">try</span> <span class="nb">constructor</span>; solve_by_inverts (S n') <span class="kr">end</span> + <span class="kr">end</span> + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Ltac</span> <span class="nf">solve_by_invert</span> := solve_by_inverts <span class="mi">1</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Ltac</span> <span class="nf">invert</span> x := <span class="nb">inversion</span> x; <span class="nb">subst</span>; <span class="nb">clear</span> x.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Ltac</span> <span class="nf">destruct_match</span> := + <span class="kr">match goal with</span> | [ |- <span class="kp">context</span>[<span class="kr">match</span> <span class="nl">?x</span> <span class="kr">with</span> | _ => _ <span class="kr">end</span> ] ] => <span class="nb">destruct</span> x <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Ltac</span> <span class="nf">nicify_hypotheses</span> := + <span class="kp">repeat</span> <span class="kr">match goal with</span> + | [ H : ex _ |- _ ] => invert H + | [ H : Some _ = Some _ |- _ ] => invert H + | [ H : <span class="nl">?x</span> = <span class="nl">?x</span> |- _ ] => <span class="nb">clear</span> H + | [ H : _ /\ _ |- _ ] => invert H + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Ltac</span> <span class="nf">nicify_goals</span> := + <span class="kp">repeat</span> <span class="kr">match goal with</span> + | [ |- _ /\ _ ] => <span class="nb">split</span> + | [ |- Some _ = Some _ ] => <span class="nb">f_equal</span> + | [ |- S _ = S _ ] => <span class="nb">f_equal</span> + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Ltac</span> <span class="nf">kill_bools</span> := + <span class="kp">repeat</span> <span class="kr">match goal with</span> + | [ H : _ && _ = true |- _ ] => <span class="nb">apply</span> andb_prop <span class="kr">in</span> H + | [ H : _ || _ = false |- _ ] => <span class="nb">apply</span> orb_false_elim <span class="kr">in</span> H + + | [ H : _ <=? _ = true |- _ ] => <span class="nb">apply</span> Z.leb_le <span class="kr">in</span> H + | [ H : _ <=? _ = false |- _ ] => <span class="nb">apply</span> Z.leb_gt <span class="kr">in</span> H + | [ H : _ <? _ = true |- _ ] => <span class="nb">apply</span> Z.ltb_lt <span class="kr">in</span> H + | [ H : _ <? _ = false |- _ ] => <span class="nb">apply</span> Z.ltb_ge <span class="kr">in</span> H + | [ H : _ >=? _ = _ |- _ ] => <span class="nb">rewrite</span> Z.geb_leb <span class="kr">in</span> H + | [ H : _ >? _ = _ |- _ ] => <span class="nb">rewrite</span> Z.gtb_ltb <span class="kr">in</span> H + + | [ H : _ =? _ = true |- _ ] => <span class="nb">apply</span> Z.eqb_eq <span class="kr">in</span> H + | [ H : _ =? _ = false |- _ ] => <span class="nb">apply</span> Z.eqb_neq <span class="kr">in</span> H + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Ltac</span> <span class="nf">unfold_constants</span> := + <span class="kp">repeat</span> <span class="kr">match goal with</span> + | [ |- <span class="kp">context</span>[Integers.Ptrofs.modulus] ] => + <span class="nb">replace</span> Integers.Ptrofs.modulus <span class="kr">with</span> <span class="mi">4294967296</span> <span class="bp">by</span> <span class="bp">reflexivity</span> + | [ H : <span class="kp">context</span>[Integers.Ptrofs.modulus] |- _ ] => + <span class="nb">replace</span> Integers.Ptrofs.modulus <span class="kr">with</span> <span class="mi">4294967296</span> <span class="kr">in</span> H <span class="bp">by</span> <span class="bp">reflexivity</span> + + | [ |- <span class="kp">context</span>[Integers.Ptrofs.min_signed] ] => + <span class="nb">replace</span> Integers.Ptrofs.min_signed <span class="kr">with</span> (-<span class="mi">2147483648</span>) <span class="bp">by</span> <span class="bp">reflexivity</span> + | [ H : <span class="kp">context</span>[Integers.Ptrofs.min_signed] |- _ ] => + <span class="nb">replace</span> Integers.Ptrofs.min_signed <span class="kr">with</span> (-<span class="mi">2147483648</span>) <span class="kr">in</span> H <span class="bp">by</span> <span class="bp">reflexivity</span> + + | [ |- <span class="kp">context</span>[Integers.Ptrofs.max_signed] ] => + <span class="nb">replace</span> Integers.Ptrofs.max_signed <span class="kr">with</span> <span class="mi">2147483647</span> <span class="bp">by</span> <span class="bp">reflexivity</span> + | [ H : <span class="kp">context</span>[Integers.Ptrofs.max_signed] |- _ ] => + <span class="nb">replace</span> Integers.Ptrofs.max_signed <span class="kr">with</span> <span class="mi">2147483647</span> <span class="kr">in</span> H <span class="bp">by</span> <span class="bp">reflexivity</span> + + | [ |- <span class="kp">context</span>[Integers.Ptrofs.max_unsigned] ] => + <span class="nb">replace</span> Integers.Ptrofs.max_unsigned <span class="kr">with</span> <span class="mi">4294967295</span> <span class="bp">by</span> <span class="bp">reflexivity</span> + | [ H : <span class="kp">context</span>[Integers.Ptrofs.max_unsigned] |- _ ] => + <span class="nb">replace</span> Integers.Ptrofs.max_unsigned <span class="kr">with</span> <span class="mi">4294967295</span> <span class="kr">in</span> H <span class="bp">by</span> <span class="bp">reflexivity</span> + + | [ |- <span class="kp">context</span>[Integers.Int.modulus] ] => + <span class="nb">replace</span> Integers.Int.modulus <span class="kr">with</span> <span class="mi">4294967296</span> <span class="bp">by</span> <span class="bp">reflexivity</span> + | [ H : <span class="kp">context</span>[Integers.Int.modulus] |- _ ] => + <span class="nb">replace</span> Integers.Int.modulus <span class="kr">with</span> <span class="mi">4294967296</span> <span class="kr">in</span> H <span class="bp">by</span> <span class="bp">reflexivity</span> + + | [ |- <span class="kp">context</span>[Integers.Int.min_signed] ] => + <span class="nb">replace</span> Integers.Int.min_signed <span class="kr">with</span> (-<span class="mi">2147483648</span>) <span class="bp">by</span> <span class="bp">reflexivity</span> + | [ H : <span class="kp">context</span>[Integers.Int.min_signed] |- _ ] => + <span class="nb">replace</span> Integers.Int.min_signed <span class="kr">with</span> (-<span class="mi">2147483648</span>) <span class="kr">in</span> H <span class="bp">by</span> <span class="bp">reflexivity</span> + + | [ |- <span class="kp">context</span>[Integers.Int.max_signed] ] => + <span class="nb">replace</span> Integers.Int.max_signed <span class="kr">with</span> <span class="mi">2147483647</span> <span class="bp">by</span> <span class="bp">reflexivity</span> + | [ H : <span class="kp">context</span>[Integers.Int.max_signed] |- _ ] => + <span class="nb">replace</span> Integers.Int.max_signed <span class="kr">with</span> <span class="mi">2147483647</span> <span class="kr">in</span> H <span class="bp">by</span> <span class="bp">reflexivity</span> + + | [ |- <span class="kp">context</span>[Integers.Int.max_unsigned] ] => + <span class="nb">replace</span> Integers.Int.max_unsigned <span class="kr">with</span> <span class="mi">4294967295</span> <span class="bp">by</span> <span class="bp">reflexivity</span> + | [ H : <span class="kp">context</span>[Integers.Int.max_unsigned] |- _ ] => + <span class="nb">replace</span> Integers.Int.max_unsigned <span class="kr">with</span> <span class="mi">4294967295</span> <span class="kr">in</span> H <span class="bp">by</span> <span class="bp">reflexivity</span> + + | [ |- <span class="kp">context</span>[Integers.Ptrofs.unsigned (Integers.Ptrofs.repr <span class="nl">?x</span>) ] ] => + <span class="kr">match</span> (<span class="kp">eval</span> <span class="nb">compute</span> <span class="kr">in</span> (<span class="mi">0</span> <=? x)) <span class="kr">with</span> + | true => <span class="nb">replace</span> (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr x)) + <span class="kr">with</span> x <span class="bp">by</span> <span class="bp">reflexivity</span> + | false => <span class="kp">idtac</span> + <span class="kr">end</span> + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Ltac</span> <span class="nf">substpp</span> := + <span class="kp">repeat</span> <span class="kr">match goal with</span> + | [ H1 : <span class="nl">?x</span> = Some _, H2 : <span class="nl">?x</span> = Some _ |- _ ] => + <span class="kr">let</span> <span class="nv">EQ</span> := <span class="kp">fresh</span> <span class="s2">"EQ"</span> <span class="kr">in</span> + learn H1 <span class="kr">as</span> EQ; <span class="nb">rewrite</span> H2 <span class="kr">in</span> EQ; invert EQ + | _ => <span class="kp">idtac</span> + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Ltac</span> <span class="nf">simplify</span> := <span class="nb">intros</span>; unfold_constants; <span class="nb">simpl</span> <span class="kr">in</span> *; + <span class="kp">repeat</span> (nicify_hypotheses; nicify_goals; kill_bools; substpp); + <span class="nb">simpl</span> <span class="kr">in</span> *.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Infix</span> <span class="s2">"==nat"</span> := eq_nat_dec (<span class="kn">no associativity</span>, <span class="kn">at level</span> <span class="mi">50</span>).</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Infix</span> <span class="s2">"==Z"</span> := Z.eq_dec (<span class="kn">no associativity</span>, <span class="kn">at level</span> <span class="mi">50</span>).</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Ltac</span> <span class="nf">liapp</span> := + <span class="kp">repeat</span> <span class="kr">match goal with</span> + | [ |- (<span class="nl">?x</span> | <span class="nl">?y</span>) ] => + <span class="kr">match</span> (<span class="kp">eval</span> <span class="nb">compute</span> <span class="kr">in</span> (Z.rem y x ==Z <span class="mi">0</span>)) <span class="kr">with</span> + | <span class="nb">left</span> _ => + <span class="kr">let</span> <span class="nv">q</span> := (<span class="kp">eval</span> <span class="nb">compute</span> <span class="kr">in</span> (Z.div y x)) + <span class="kr">in</span> <span class="kr">exists</span> <span class="nv">q</span>; <span class="bp">reflexivity</span> + | _ => <span class="kp">idtac</span> + <span class="kr">end</span> + | _ => <span class="kp">idtac</span> + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Ltac</span> <span class="nf">crush</span> := simplify; <span class="kp">try</span> <span class="bp">discriminate</span>; <span class="kp">try</span> <span class="bp">congruence</span>; <span class="kp">try</span> <span class="bp">lia</span>; liapp; <span class="kp">try</span> <span class="bp">assumption</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Global Opaque</span> Nat.div.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Global Opaque</span> Z.mul.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +<span class="c">(* Definition const (A B : Type) (a : A) (b : B) : A := a.</span> + +<span class="c">Definition compose (A B C : Type) (f : B -> C) (g : A -> B) (x : A) : C := f (g x). *)</span> + +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Module</span> <span class="nf">Option</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">default</span> {<span class="nv">T</span> : <span class="kt">Type</span>} (<span class="nv">x</span> : T) (<span class="nv">u</span> : option T) : T := + <span class="kr">match</span> u <span class="kr">with</span> + | Some y => y + | _ => x + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">map</span> {<span class="nv">S</span> : <span class="kt">Type</span>} {<span class="nv">T</span> : <span class="kt">Type</span>} (<span class="nv">f</span> : S -> T) (<span class="nv">u</span> : option S) : option T := + <span class="kr">match</span> u <span class="kr">with</span> + | Some y => Some (f y) + | _ => None + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">liftA2</span> {<span class="nv">T</span> : <span class="kt">Type</span>} (<span class="nv">f</span> : T -> T -> T) (<span class="nv">a</span> : option T) (<span class="nv">b</span> : option T) : option T := + <span class="kr">match</span> a <span class="kr">with</span> + | Some x => map (f x) b + | _ => None + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">bind</span> {<span class="nv">A</span> <span class="nv">B</span> : <span class="kt">Type</span>} (<span class="nv">f</span> : option A) (<span class="nv">g</span> : A -> option B) : option B := + <span class="kr">match</span> f <span class="kr">with</span> + | Some a => g a + | _ => None + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">join</span> {<span class="nv">A</span> : <span class="kt">Type</span>} (<span class="nv">a</span> : option (option A)) : option A := + <span class="kr">match</span> a <span class="kr">with</span> + | None => None + | Some a' => a' + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Module</span> <span class="nf">Notation</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Notation</span> <span class="s2">"'do' X <- A ; B"</span> := (bind A (<span class="kr">fun</span> <span class="nv">X</span> => B)) + (<span class="kn">at level</span> <span class="mi">200</span>, X <span class="kn">ident</span>, A <span class="kn">at level</span> <span class="mi">100</span>, B <span class="kn">at level</span> <span class="mi">200</span>).</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">End</span> <span class="nf">Notation</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">End</span> <span class="nf">Option</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Parameter</span> <span class="nv">debug_print</span> : string -> unit.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">debug_show</span> {<span class="nv">A</span> <span class="nv">B</span> : <span class="kt">Type</span>} `{<span class="kn">Show</span> A} (a : A) (b : B) : B := + <span class="kr">let</span> <span class="nv">unused</span> := debug_print (show a) <span class="kr">in</span> b.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">debug_show_msg</span> {<span class="nv">A</span> <span class="nv">B</span> : <span class="kt">Type</span>} `{<span class="kn">Show</span> A} (s : string) (a : A) (b : B) : B := + <span class="kr">let</span> <span class="nv">unused</span> := debug_print (s ++ show a) <span class="kr">in</span> b.</span></span></span></pre> +</div> +</div></body> +</html> |