https://github.com/uds-psl/cook-levin
Tip revision: e24a92af25746f6758a09ea1dc51e57491508e60 authored by Fabian Kunze on 03 February 2021, 23:29:51 UTC
added missing html doc
added missing html doc
Tip revision: e24a92a
Undecidability.Shared.embed_nat.html
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
<link href="coqdocjs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="config.js"></script>
<script type="text/javascript" src="coqdocjs.js"></script>
</head>
<body onload="document.getElementById('content').focus()">
<div id="header">
<span class="left">
<span class="modulename"> <script> document.write(document.title) </script> </span>
</span>
<span class="button" id="toggle-proofs"></span>
<span class="right">
<a href="../">Project Page</a>
<a href="./indexpage.html"> Index </a>
<a href="./toc.html"> Table of Contents </a>
</span>
</div>
<div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
<div id="main">
<div class="code">
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#"><span class="id" title="library">PeanoNat</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="embed" class="idref" href="#embed"><span class="id" title="definition">embed</span></a> <a id="pat:3" class="idref" href="#pat:3"><span class="id" title="binder">'(</span></a><a id="pat:3" class="idref" href="#pat:3"><span class="id" title="binder">x</span></a><a id="pat:3" class="idref" href="#pat:3"><span class="id" title="binder">,</span></a> <a id="pat:3" class="idref" href="#pat:3"><span class="id" title="binder">y</span></a><a id="pat:3" class="idref" href="#pat:3"><span class="id" title="binder">)</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> := <br/>
<a class="idref" href="Undecidability.Shared.embed_nat.html#y:1"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#nat_rec"><span class="id" title="definition">nat_rec</span></a> <span class="id" title="var">_</span> 0 (<span class="id" title="keyword">fun</span> <a id="i:4" class="idref" href="#i:4"><span class="id" title="binder">i</span></a> <a id="m:5" class="idref" href="#m:5"><span class="id" title="binder">m</span></a> => <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Undecidability.Shared.embed_nat.html#i:4"><span class="id" title="variable">i</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="Undecidability.Shared.embed_nat.html#m:5"><span class="id" title="variable">m</span></a>) (<a class="idref" href="Undecidability.Shared.embed_nat.html#y:1"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="Undecidability.Shared.embed_nat.html#x:2"><span class="id" title="variable">x</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">)</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="unembed" class="idref" href="#unembed"><span class="id" title="definition">unembed</span></a> (<a id="n:6" class="idref" href="#n:6"><span class="id" title="binder">n</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> := <br/>
<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#nat_rec"><span class="id" title="definition">nat_rec</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a>0<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> <a id="pat:9" class="idref" href="#pat:9"><span class="id" title="binder">'(</span></a><a id="pat:9" class="idref" href="#pat:9"><span class="id" title="binder">x</span></a><a id="pat:9" class="idref" href="#pat:9"><span class="id" title="binder">,</span></a> <a id="pat:9" class="idref" href="#pat:9"><span class="id" title="binder">y</span></a><a id="pat:9" class="idref" href="#pat:9"><span class="id" title="binder">)</span></a> => <span class="id" title="keyword">match</span> <a class="idref" href="Undecidability.Shared.embed_nat.html#x:8"><span class="id" title="variable">x</span></a> <span class="id" title="keyword">with</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">x</span> => <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Undecidability.Shared.embed_nat.html#x:8"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Undecidability.Shared.embed_nat.html#y:7"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> | <span class="id" title="var">_</span> => <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Undecidability.Shared.embed_nat.html#y:7"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> <span class="id" title="keyword">end</span>) <a class="idref" href="Undecidability.Shared.embed_nat.html#n:6"><span class="id" title="variable">n</span></a>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="embedP" class="idref" href="#embedP"><span class="id" title="lemma">embedP</span></a> {<a id="xy:11" class="idref" href="#xy:11"><span class="id" title="binder">xy</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>} : <a class="idref" href="Undecidability.Shared.embed_nat.html#unembed"><span class="id" title="definition">unembed</span></a> (<a class="idref" href="Undecidability.Shared.embed_nat.html#embed"><span class="id" title="definition">embed</span></a> <a class="idref" href="Undecidability.Shared.embed_nat.html#xy:11"><span class="id" title="variable">xy</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Undecidability.Shared.embed_nat.html#xy:11"><span class="id" title="variable">xy</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">assert</span> (<span class="id" title="keyword">forall</span> <a id="n:13" class="idref" href="#n:13"><span class="id" title="binder">n</span></a>, <a class="idref" href="Undecidability.Shared.embed_nat.html#embed"><span class="id" title="definition">embed</span></a> <span class="id" title="var">xy</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Undecidability.Shared.embed_nat.html#n:12"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Undecidability.Shared.embed_nat.html#unembed"><span class="id" title="definition">unembed</span></a> <a class="idref" href="Undecidability.Shared.embed_nat.html#n:12"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="var">xy</span>).<br/>
<span class="id" title="tactic">intro</span> <span class="id" title="var">n</span>. <span class="id" title="var">revert</span> <span class="id" title="var">xy</span>. <span class="id" title="tactic">induction</span> <span class="id" title="var">n</span> <span class="id" title="keyword">as</span> [|<span class="id" title="var">n</span> <span class="id" title="var">IH</span>].<br/>
<span class="id" title="tactic">intros</span> [[|?] [|?]]; <span class="id" title="tactic">intro</span> <span class="id" title="var">H</span>; <span class="id" title="tactic">inversion</span> <span class="id" title="var">H</span>; <span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="tactic">intros</span> [<span class="id" title="var">x</span> [|<span class="id" title="var">y</span>]]; <span class="id" title="tactic">simpl</span>.<br/>
<span class="id" title="tactic">case</span> <span class="id" title="var">x</span> <span class="id" title="keyword">as</span> [|<span class="id" title="var">x</span>]; <span class="id" title="tactic">simpl</span>; <span class="id" title="tactic">intro</span> <span class="id" title="var">H</span>.<br/>
<span class="id" title="tactic">inversion</span> <span class="id" title="var">H</span>.<br/>
<span class="id" title="tactic">rewrite</span> (<span class="id" title="var">IH</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a>0<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>); [<span class="id" title="tactic">reflexivity</span>|].<br/>
<span class="id" title="tactic">inversion</span> <span class="id" title="var">H</span>; <span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">rewrite</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#Nat.add_0_r"><span class="id" title="lemma">Nat.add_0_r</span></a>. <span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="tactic">intro</span> <span class="id" title="var">H</span>. <span class="id" title="tactic">rewrite</span> (<span class="id" title="var">IH</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">y</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>); [<span class="id" title="tactic">reflexivity</span>|].<br/>
<span class="id" title="tactic">inversion</span> <span class="id" title="var">H</span>. <span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">rewrite</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#Nat.add_succ_r"><span class="id" title="lemma">Nat.add_succ_r</span></a>. <span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="tactic">apply</span> <span class="id" title="var">H</span>. <span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="unembedP" class="idref" href="#unembedP"><span class="id" title="lemma">unembedP</span></a> {<a id="n:14" class="idref" href="#n:14"><span class="id" title="binder">n</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>} : <a class="idref" href="Undecidability.Shared.embed_nat.html#embed"><span class="id" title="definition">embed</span></a> (<a class="idref" href="Undecidability.Shared.embed_nat.html#unembed"><span class="id" title="definition">unembed</span></a> <a class="idref" href="Undecidability.Shared.embed_nat.html#n:14"><span class="id" title="variable">n</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Undecidability.Shared.embed_nat.html#n:14"><span class="id" title="variable">n</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">induction</span> <span class="id" title="var">n</span> <span class="id" title="keyword">as</span> [|<span class="id" title="var">n</span> <span class="id" title="var">IH</span>]; [<span class="id" title="tactic">reflexivity</span>|].<br/>
<span class="id" title="tactic">simpl</span>. <span class="id" title="var">revert</span> <span class="id" title="var">IH</span>. <span class="id" title="tactic">case</span> (<a class="idref" href="Undecidability.Shared.embed_nat.html#unembed"><span class="id" title="definition">unembed</span></a> <span class="id" title="var">n</span>). <span class="id" title="tactic">intros</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>.<br/>
<span class="id" title="tactic">case</span> <span class="id" title="var">x</span> <span class="id" title="keyword">as</span> [|<span class="id" title="var">x</span>]; <span class="id" title="tactic">intro</span> <span class="id" title="var">Hx</span>; <span class="id" title="tactic">rewrite</span> <- <span class="id" title="var">Hx</span>; <span class="id" title="tactic">simpl</span>.<br/>
<span class="id" title="tactic">rewrite</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#Nat.add_0_r"><span class="id" title="lemma">Nat.add_0_r</span></a>. <span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="tactic">rewrite</span> ?<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#Nat.add_succ_r"><span class="id" title="lemma">Nat.add_succ_r</span></a>. <span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">rewrite</span> ?<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#Nat.add_succ_r"><span class="id" title="lemma">Nat.add_succ_r</span></a>. <span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<span class="id" title="var">Arguments</span> <a class="idref" href="Undecidability.Shared.embed_nat.html#embed"><span class="id" title="definition">embed</span></a> : <span class="id" title="tactic">simpl</span> <span class="id" title="var">never</span>.<br/>
<br/>
<span class="id" title="keyword">Module</span> <a id="EmbedNatNotations" class="idref" href="#EmbedNatNotations"><span class="id" title="module">EmbedNatNotations</span></a>.<br/>
<span class="id" title="keyword">Notation</span> <a id="37369fe30ff349fb35263eabcb59bd96" class="idref" href="#37369fe30ff349fb35263eabcb59bd96"><span class="id" title="notation">"</span></a>⟨ a , b ⟩" := (<a class="idref" href="Undecidability.Shared.embed_nat.html#embed"><span class="id" title="definition">embed</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">a</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">b</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0).<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Undecidability.Shared.embed_nat.html#EmbedNatNotations"><span class="id" title="module">EmbedNatNotations</span></a>.<br/>
</div>
</div>
<div id="footer">
Generated by <a href="http://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/tebbi/coqdocjs">CoqdocJS</a>
</div>
</div>
</body>
</html>
