Skip to content

Commit 43b800e

Browse files
committed
r4195
1 parent 9dc6bcc commit 43b800e

File tree

339 files changed

+435
-424
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

339 files changed

+435
-424
lines changed

lf-current/AltAuto.html

Lines changed: 11 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1520,6 +1520,13 @@ <h1 class="libtitle">AltAuto<span class="subtitle">A Streamlined Treatment of Au
15201520
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Poly.html#length"><span class="id" title="definition">length</span></a> <a class="idref" href="AltAuto.html#s<sub>1</sub>:159"><span class="id" title="variable">s<sub>1</sub></span></a> <a class="idref" href="Basics.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="Poly.html#length"><span class="id" title="definition">length</span></a> <a class="idref" href="AltAuto.html#s<sub>2</sub>:160"><span class="id" title="variable">s<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#cb53cf0ee22c036a03b4a9281c68b5a<sub>3</sub>"><span class="id" title="notation"></span></a> <a class="idref" href="IndProp.html#Pumping.pumping_constant"><span class="id" title="definition">pumping_constant</span></a> <a class="idref" href="AltAuto.html#re:157"><span class="id" title="variable">re</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation"></span></a><br/>
15211521
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword"></span> <a id="m:162" class="idref" href="#m:162"><span class="id" title="binder">m</span></a>, <a class="idref" href="AltAuto.html#s<sub>1</sub>:159"><span class="id" title="variable">s<sub>1</sub></span></a> <a class="idref" href="Poly.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a> <a class="idref" href="IndProp.html#Pumping.napp"><span class="id" title="definition">napp</span></a> <a class="idref" href="AltAuto.html#m:162"><span class="id" title="variable">m</span></a> <a class="idref" href="AltAuto.html#s<sub>2</sub>:160"><span class="id" title="variable">s<sub>2</sub></span></a> <a class="idref" href="Poly.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a> <a class="idref" href="AltAuto.html#s<sub>3</sub>:161"><span class="id" title="variable">s<sub>3</sub></span></a> <a class="idref" href="IndProp.html#70ea788eca33f3ac1bb7ed2e8169c791"><span class="id" title="notation">=~</span></a> <a class="idref" href="AltAuto.html#re:157"><span class="id" title="variable">re</span></a>.<br/><hr class='doublespaceincode'/>
15221522
<span class="id" title="keyword">Proof</span>.<br/>
1523+
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">T</span> <span class="id" title="var">re</span> <span class="id" title="var">s</span> <span class="id" title="var">Hmatch</span>.<br/>
1524+
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">Hmatch</span><br/>
1525+
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">as</span> [ | <span class="id" title="var">x</span> | <span class="id" title="var">s<sub>1</sub></span> <span class="id" title="var">re<sub>1</sub></span> <span class="id" title="var">s<sub>2</sub></span> <span class="id" title="var">re<sub>2</sub></span> <span class="id" title="var">Hmatch1</span> <span class="id" title="var">IH<sub>1</sub></span> <span class="id" title="var">Hmatch2</span> <span class="id" title="var">IH<sub>2</sub></span><br/>
1526+
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">s<sub>1</sub></span> <span class="id" title="var">re<sub>1</sub></span> <span class="id" title="var">re<sub>2</sub></span> <span class="id" title="var">Hmatch</span> <span class="id" title="var">IH</span> | <span class="id" title="var">re<sub>1</sub></span> <span class="id" title="var">s<sub>2</sub></span> <span class="id" title="var">re<sub>2</sub></span> <span class="id" title="var">Hmatch</span> <span class="id" title="var">IH</span><br/>
1527+
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">re</span> | <span class="id" title="var">s<sub>1</sub></span> <span class="id" title="var">s<sub>2</sub></span> <span class="id" title="var">re</span> <span class="id" title="var">Hmatch1</span> <span class="id" title="var">IH<sub>1</sub></span> <span class="id" title="var">Hmatch2</span> <span class="id" title="var">IH<sub>2</sub></span> ];<br/>
1528+
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">simpl</span>; <span class="id" title="tactic">try</span> <span class="id" title="var">lia</span>;<br/>
1529+
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">Hlen</span>.<br/>
15231530
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
15241531
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
15251532
<span class="id" title="keyword">Definition</span> <a id="manual_grade_for_pumping_redux_strong" class="idref" href="#manual_grade_for_pumping_redux_strong"><span class="id" title="definition">manual_grade_for_pumping_redux_strong</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="IndProp.html#string"><span class="id" title="definition">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
@@ -1545,7 +1552,7 @@ <h1 class="libtitle">AltAuto<span class="subtitle">A Streamlined Treatment of Au
15451552
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="AltAuto.html#a:163"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#cb53cf0ee22c036a03b4a9281c68b5a<sub>3</sub>"><span class="id" title="notation"></span></a> <a class="idref" href="AltAuto.html#d:166"><span class="id" title="variable">d</span></a>.<br/>
15461553
<span class="id" title="keyword">Proof</span>.<br/>
15471554
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span> <span class="id" title="var">c</span> <span class="id" title="var">d</span> <span class="id" title="var">H<sub>1</sub></span> <span class="id" title="var">H<sub>2</sub></span>.<br/>
1548-
&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="IndProp.html#le_trans"><span class="id" title="axiom">le_trans</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">b</span> <a class="idref" href="Basics.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <span class="id" title="var">b</span> <a class="idref" href="Basics.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">×</span></a> <span class="id" title="var">c</span>).<br/>
1555+
&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Arith.PeanoNat.html#Nat.le_trans"><span class="id" title="lemma">Nat.le_trans</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">b</span> <a class="idref" href="Basics.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <span class="id" title="var">b</span> <a class="idref" href="Basics.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">×</span></a> <span class="id" title="var">c</span>).<br/>
15491556
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;^&nbsp;We&nbsp;must&nbsp;supply&nbsp;the&nbsp;intermediate&nbsp;value&nbsp;*)</span><br/>
15501557
&nbsp;&nbsp;- <span class="id" title="tactic">apply</span> <span class="id" title="var">H<sub>1</sub></span>.<br/>
15511558
&nbsp;&nbsp;- <span class="id" title="tactic">simpl</span> <span class="id" title="keyword">in</span> <span class="id" title="var">H<sub>2</sub></span>. <span class="id" title="tactic">rewrite</span> <a class="idref" href="Induction.html#mul_comm"><span class="id" title="axiom">mul_comm</span></a>. <span class="id" title="tactic">apply</span> <span class="id" title="var">H<sub>2</sub></span>.<br/>
@@ -1579,7 +1586,7 @@ <h1 class="libtitle">AltAuto<span class="subtitle">A Streamlined Treatment of Au
15791586
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="AltAuto.html#a:167"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#cb53cf0ee22c036a03b4a9281c68b5a<sub>3</sub>"><span class="id" title="notation"></span></a> <a class="idref" href="AltAuto.html#d:170"><span class="id" title="variable">d</span></a>.<br/>
15801587
<span class="id" title="keyword">Proof</span>.<br/>
15811588
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span> <span class="id" title="var">c</span> <span class="id" title="var">d</span> <span class="id" title="var">H<sub>1</sub></span> <span class="id" title="var">H<sub>2</sub></span>.<br/>
1582-
&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="IndProp.html#le_trans"><span class="id" title="axiom">le_trans</span></a>. <span class="comment">(*&nbsp;1&nbsp;*)</span><br/>
1589+
&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Arith.PeanoNat.html#Nat.le_trans"><span class="id" title="lemma">Nat.le_trans</span></a>. <span class="comment">(*&nbsp;1&nbsp;*)</span><br/>
15831590
&nbsp;&nbsp;- <span class="id" title="tactic">apply</span> <span class="id" title="var">H<sub>1</sub></span>. <span class="comment">(*&nbsp;2&nbsp;*)</span><br/>
15841591
&nbsp;&nbsp;- <span class="id" title="tactic">simpl</span> <span class="id" title="keyword">in</span> <span class="id" title="var">H<sub>2</sub></span>. <span class="id" title="tactic">rewrite</span> <a class="idref" href="Induction.html#mul_comm"><span class="id" title="axiom">mul_comm</span></a>. <span class="id" title="tactic">apply</span> <span class="id" title="var">H<sub>2</sub></span>.<br/>
15851592
<span class="id" title="keyword">Qed</span>.<br/>
@@ -1615,7 +1622,7 @@ <h1 class="libtitle">AltAuto<span class="subtitle">A Streamlined Treatment of Au
16151622
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="AltAuto.html#a:171"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#cb53cf0ee22c036a03b4a9281c68b5a<sub>3</sub>"><span class="id" title="notation"></span></a> <a class="idref" href="AltAuto.html#d:174"><span class="id" title="variable">d</span></a>.<br/>
16161623
<span class="id" title="keyword">Proof</span>.<br/>
16171624
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span> <span class="id" title="var">c</span> <span class="id" title="var">d</span> <span class="id" title="var">H<sub>1</sub></span> <span class="id" title="var">H<sub>2</sub></span>.<br/>
1618-
&nbsp;&nbsp;<span class="id" title="tactic">info_eauto</span> <span class="id" title="keyword">using</span> <a class="idref" href="IndProp.html#le_trans"><span class="id" title="axiom">le_trans</span></a>.<br/>
1625+
&nbsp;&nbsp;<span class="id" title="tactic">info_eauto</span> <span class="id" title="keyword">using</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Arith.PeanoNat.html#Nat.le_trans"><span class="id" title="lemma">Nat.le_trans</span></a>.<br/>
16191626
<span class="id" title="keyword">Qed</span>.<br/>
16201627
</div>
16211628

@@ -2410,7 +2417,7 @@ <h1 class="libtitle">AltAuto<span class="subtitle">A Streamlined Treatment of Au
24102417
</div>
24112418
<div class="code">
24122419

2413-
<span class="comment">(*&nbsp;2024-08-25&nbsp;18:03&nbsp;*)</span><br/>
2420+
<span class="comment">(*&nbsp;2024-08-30&nbsp;14:17&nbsp;*)</span><br/>
24142421
</div>
24152422
</div>
24162423

lf-current/AltAuto.v

Lines changed: 11 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1180,6 +1180,13 @@ Lemma pumping : forall T (re : reg_exp T) s,
11801180
forall m, s1 ++ napp m s2 ++ s3 =~ re.
11811181

11821182
Proof.
1183+
intros T re s Hmatch.
1184+
induction Hmatch
1185+
as [ | x | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
1186+
| s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
1187+
| re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2 ];
1188+
simpl; try lia;
1189+
intros Hlen.
11831190
(* FILL IN HERE *) Admitted.
11841191
(* Do not modify the following line: *)
11851192
Definition manual_grade_for_pumping_redux_strong : option (nat*string) := None.
@@ -1199,7 +1206,7 @@ Example trans_example1: forall a b c d,
11991206
a <= d.
12001207
Proof.
12011208
intros a b c d H1 H2.
1202-
apply le_trans with (b + b * c).
1209+
apply Nat.le_trans with (b + b * c).
12031210
(* ^ We must supply the intermediate value *)
12041211
- apply H1.
12051212
- simpl in H2. rewrite mul_comm. apply H2.
@@ -1228,7 +1235,7 @@ Example trans_example1': forall a b c d,
12281235
a <= d.
12291236
Proof.
12301237
intros a b c d H1 H2.
1231-
eapply le_trans. (* 1 *)
1238+
eapply Nat.le_trans. (* 1 *)
12321239
- apply H1. (* 2 *)
12331240
- simpl in H2. rewrite mul_comm. apply H2.
12341241
Qed.
@@ -1257,7 +1264,7 @@ Example trans_example2: forall a b c d,
12571264
a <= d.
12581265
Proof.
12591266
intros a b c d H1 H2.
1260-
info_eauto using le_trans.
1267+
info_eauto using Nat.le_trans.
12611268
Qed.
12621269

12631270
(** The [eauto] tactic works just like [auto], except that it
@@ -1825,4 +1832,4 @@ Definition manual_grade_for_nor_intuition : option (nat*string) := None.
18251832
18261833
- Ltac functions and [match goal] *)
18271834

1828-
(* 2024-08-25 18:03 *)
1835+
(* 2024-08-30 14:17 *)

lf-current/AltAutoTest.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -255,4 +255,4 @@ idtac "---------- nor_intuition ---------".
255255
idtac "MANUAL".
256256
Abort.
257257

258-
(* 2024-08-25 18:03 *)
258+
(* 2024-08-30 14:17 *)

lf-current/Auto.html

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -910,7 +910,7 @@ <h1 class="libtitle">Auto<span class="subtitle">More Automation</span></h1>
910910
<span class="id" title="keyword">Proof</span>.<br/>
911911
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">P</span> <span class="id" title="var">Q</span> <span class="id" title="var">HP</span> <span class="id" title="var">HQ</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">HP</span> <span class="id" title="keyword">as</span> [<span class="id" title="var">y</span> <span class="id" title="var">HP'</span>]. <span class="id" title="tactic">eauto</span>.<br/>
912912
<span class="id" title="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
913-
<span class="comment">(*&nbsp;2024-08-25&nbsp;18:03&nbsp;*)</span><br/>
913+
<span class="comment">(*&nbsp;2024-08-30&nbsp;14:17&nbsp;*)</span><br/>
914914
</div>
915915
</div>
916916

lf-current/Auto.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -740,4 +740,4 @@ Proof.
740740
intros P Q HP HQ. destruct HP as [y HP']. eauto.
741741
Qed.
742742

743-
(* 2024-08-25 18:03 *)
743+
(* 2024-08-30 14:17 *)

lf-current/AutoTest.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -63,4 +63,4 @@ idtac "".
6363
idtac "********** Advanced **********".
6464
Abort.
6565

66-
(* 2024-08-25 18:03 *)
66+
(* 2024-08-30 14:17 *)

lf-current/Basics.html

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2691,7 +2691,7 @@ <h1 class="libtitle">Basics<span class="subtitle">Functional Programming in Coq<
26912691
</div>
26922692
<div class="code">
26932693

2694-
<span class="comment">(*&nbsp;2024-08-25&nbsp;18:02&nbsp;*)</span><br/>
2694+
<span class="comment">(*&nbsp;2024-08-30&nbsp;14:17&nbsp;*)</span><br/>
26952695
</div>
26962696
</div>
26972697

lf-current/Basics.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2015,4 +2015,4 @@ Example test_bin_incr6 :
20152015
output. But since they have to be graded by a human, the test
20162016
script won't be able to tell you much about them. *)
20172017

2018-
(* 2024-08-25 18:02 *)
2018+
(* 2024-08-30 14:17 *)

lf-current/BasicsTest.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -521,4 +521,4 @@ idtac "".
521521
idtac "********** Advanced **********".
522522
Abort.
523523

524-
(* 2024-08-25 18:03 *)
524+
(* 2024-08-30 14:17 *)

lf-current/Bib.html

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,7 @@ <h1 class="libtitle">Bib<span class="subtitle">Bibliography</span></h1>
8484
</div>
8585
<div class="code">
8686

87-
<span class="comment">(*&nbsp;2024-08-25&nbsp;18:03&nbsp;*)</span><br/>
87+
<span class="comment">(*&nbsp;2024-08-30&nbsp;14:17&nbsp;*)</span><br/>
8888
</div>
8989
</div>
9090

0 commit comments

Comments
 (0)