diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /theories/Program | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'theories/Program')
-rw-r--r-- | theories/Program/Basics.v | 10 | ||||
-rw-r--r-- | theories/Program/Combinators.v | 22 | ||||
-rw-r--r-- | theories/Program/Equality.v | 10 | ||||
-rw-r--r-- | theories/Program/Program.v | 10 | ||||
-rw-r--r-- | theories/Program/Subset.v | 10 | ||||
-rw-r--r-- | theories/Program/Syntax.v | 10 | ||||
-rw-r--r-- | theories/Program/Tactics.v | 12 | ||||
-rw-r--r-- | theories/Program/Utils.v | 10 | ||||
-rw-r--r-- | theories/Program/Wf.v | 11 | ||||
-rw-r--r-- | theories/Program/vo.itarget | 9 |
10 files changed, 59 insertions, 55 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index 644b9b5a..f55093ed 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -1,10 +1,12 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Standard functions and combinators. diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v index 772018aa..f78d06b1 100644 --- a/theories/Program/Combinators.v +++ b/theories/Program/Combinators.v @@ -1,10 +1,12 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** * Proofs about standard combinators, exports functional extensionality. @@ -22,15 +24,13 @@ Open Scope program_scope. Lemma compose_id_left : forall A B (f : A -> B), id ∘ f = f. Proof. intros. - unfold id, compose. - symmetry. apply eta_expansion. + reflexivity. Qed. Lemma compose_id_right : forall A B (f : A -> B), f ∘ id = f. Proof. intros. - unfold id, compose. - symmetry ; apply eta_expansion. + reflexivity. Qed. Lemma compose_assoc : forall A B C D (f : A -> B) (g : B -> C) (h : C -> D), @@ -47,9 +47,7 @@ Hint Rewrite <- @compose_assoc : core. Lemma flip_flip : forall A B C, @flip A B C ∘ flip = id. Proof. - unfold flip, compose. intros. - extensionality x ; extensionality y ; extensionality z. reflexivity. Qed. @@ -57,9 +55,7 @@ Qed. Lemma prod_uncurry_curry : forall A B C, @prod_uncurry A B C ∘ prod_curry = id. Proof. - simpl ; intros. - unfold prod_uncurry, prod_curry, compose. - extensionality x ; extensionality y ; extensionality z. + intros. reflexivity. Qed. diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index d6f9bb9d..cf42ed18 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Tactics related to (dependent) equality and proof irrelevance. *) diff --git a/theories/Program/Program.v b/theories/Program/Program.v index 4a6f2786..de0a6d5d 100644 --- a/theories/Program/Program.v +++ b/theories/Program/Program.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Export Coq.Program.Utils. Require Export Coq.Program.Wf. diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index 2a3ec926..1c89b6c3 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Tactics related to subsets and proof irrelevance. *) diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index 2fccf624..785b9437 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Custom notations and implicits for Coq prelude definitions. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index dfd6b0ea..bc838818 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This module implements various tactics used to simplify the goals produced by Program, @@ -328,4 +330,4 @@ Ltac program_simpl := program_simplify ; try typeclasses eauto with program ; tr Obligation Tactic := program_simpl. -Definition obligation (A : Type) {a : A} := a.
\ No newline at end of file +Definition obligation (A : Type) {a : A} := a. diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index 396c9618..78c36dc7 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Various syntactic shorthands that are useful with [Program]. *) diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index c490ea51..62787985 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Reformulation of the Wf module using subsets where possible, providing the support for [Program]'s treatment of well-founded definitions. *) @@ -69,6 +71,7 @@ Section Well_founded. End Well_founded. +Require Coq.extraction.Extraction. Extraction Inline Fix_F_sub Fix_sub. Set Implicit Arguments. diff --git a/theories/Program/vo.itarget b/theories/Program/vo.itarget deleted file mode 100644 index 864c815a..00000000 --- a/theories/Program/vo.itarget +++ /dev/null @@ -1,9 +0,0 @@ -Basics.vo -Combinators.vo -Equality.vo -Program.vo -Subset.vo -Syntax.vo -Tactics.vo -Utils.vo -Wf.vo |