From d54b8dff818f0b1218df14cfb2b813da93154fa9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 12 Apr 2018 09:54:36 +0200 Subject: remove ssrtest: it now belongs to Coq --- mathcomp/Make | 46 ------ mathcomp/ssrtest/Make | 46 ------ mathcomp/ssrtest/Makefile | 25 --- mathcomp/ssrtest/absevarprop.v | 90 ----------- mathcomp/ssrtest/abstract_var2.v | 16 -- mathcomp/ssrtest/binders.v | 46 ------ mathcomp/ssrtest/binders_of.v | 14 -- mathcomp/ssrtest/caseview.v | 7 - mathcomp/ssrtest/congr.v | 26 --- mathcomp/ssrtest/deferclear.v | 29 ---- mathcomp/ssrtest/dependent_type_err.v | 11 -- mathcomp/ssrtest/derive_inversion.v | 19 --- mathcomp/ssrtest/elim.v | 297 ---------------------------------- mathcomp/ssrtest/elim2.v | 63 -------- mathcomp/ssrtest/elim_pattern.v | 19 --- mathcomp/ssrtest/explain_match.v | 13 -- mathcomp/ssrtest/first_n.v | 12 -- mathcomp/ssrtest/gen_have.v | 165 ------------------- mathcomp/ssrtest/gen_pattern.v | 24 --- mathcomp/ssrtest/have_TC.v | 40 ----- mathcomp/ssrtest/have_transp.v | 41 ----- mathcomp/ssrtest/have_view_idiom.v | 9 -- mathcomp/ssrtest/havesuff.v | 75 --------- mathcomp/ssrtest/if_isnt.v | 13 -- mathcomp/ssrtest/indetLHS.v | 8 - mathcomp/ssrtest/intro_beta.v | 15 -- mathcomp/ssrtest/intro_noop.v | 28 ---- mathcomp/ssrtest/ipatalternation.v | 8 - mathcomp/ssrtest/ltac_have.v | 32 ---- mathcomp/ssrtest/ltac_in.v | 18 --- mathcomp/ssrtest/move_after.v | 9 -- mathcomp/ssrtest/multiview.v | 60 ------- mathcomp/ssrtest/occarrow.v | 15 -- mathcomp/ssrtest/patnoX.v | 9 -- mathcomp/ssrtest/primproj.v | 157 ------------------ mathcomp/ssrtest/rewpatterns.v | 181 --------------------- mathcomp/ssrtest/set_lamda.v | 18 --- mathcomp/ssrtest/set_pattern.v | 57 ------- mathcomp/ssrtest/ssrsyntax1.v | 26 --- mathcomp/ssrtest/ssrsyntax2.v | 11 -- mathcomp/ssrtest/tc.v | 32 ---- mathcomp/ssrtest/testmx.v | 37 ----- mathcomp/ssrtest/typeof.v | 12 -- mathcomp/ssrtest/unfold_Opaque.v | 8 - mathcomp/ssrtest/unkeyed.v | 22 --- mathcomp/ssrtest/view_case.v | 22 --- mathcomp/ssrtest/wlog_suff.v | 19 --- mathcomp/ssrtest/wlogletin.v | 40 ----- mathcomp/ssrtest/wlong_intro.v | 10 -- 49 files changed, 2000 deletions(-) delete mode 100644 mathcomp/ssrtest/Make delete mode 100644 mathcomp/ssrtest/Makefile delete mode 100644 mathcomp/ssrtest/absevarprop.v delete mode 100644 mathcomp/ssrtest/abstract_var2.v delete mode 100644 mathcomp/ssrtest/binders.v delete mode 100644 mathcomp/ssrtest/binders_of.v delete mode 100644 mathcomp/ssrtest/caseview.v delete mode 100644 mathcomp/ssrtest/congr.v delete mode 100644 mathcomp/ssrtest/deferclear.v delete mode 100644 mathcomp/ssrtest/dependent_type_err.v delete mode 100644 mathcomp/ssrtest/derive_inversion.v delete mode 100644 mathcomp/ssrtest/elim.v delete mode 100644 mathcomp/ssrtest/elim2.v delete mode 100644 mathcomp/ssrtest/elim_pattern.v delete mode 100644 mathcomp/ssrtest/explain_match.v delete mode 100644 mathcomp/ssrtest/first_n.v delete mode 100644 mathcomp/ssrtest/gen_have.v delete mode 100644 mathcomp/ssrtest/gen_pattern.v delete mode 100644 mathcomp/ssrtest/have_TC.v delete mode 100644 mathcomp/ssrtest/have_transp.v delete mode 100644 mathcomp/ssrtest/have_view_idiom.v delete mode 100644 mathcomp/ssrtest/havesuff.v delete mode 100644 mathcomp/ssrtest/if_isnt.v delete mode 100644 mathcomp/ssrtest/indetLHS.v delete mode 100644 mathcomp/ssrtest/intro_beta.v delete mode 100644 mathcomp/ssrtest/intro_noop.v delete mode 100644 mathcomp/ssrtest/ipatalternation.v delete mode 100644 mathcomp/ssrtest/ltac_have.v delete mode 100644 mathcomp/ssrtest/ltac_in.v delete mode 100644 mathcomp/ssrtest/move_after.v delete mode 100644 mathcomp/ssrtest/multiview.v delete mode 100644 mathcomp/ssrtest/occarrow.v delete mode 100644 mathcomp/ssrtest/patnoX.v delete mode 100644 mathcomp/ssrtest/primproj.v delete mode 100644 mathcomp/ssrtest/rewpatterns.v delete mode 100644 mathcomp/ssrtest/set_lamda.v delete mode 100644 mathcomp/ssrtest/set_pattern.v delete mode 100644 mathcomp/ssrtest/ssrsyntax1.v delete mode 100644 mathcomp/ssrtest/ssrsyntax2.v delete mode 100644 mathcomp/ssrtest/tc.v delete mode 100644 mathcomp/ssrtest/testmx.v delete mode 100644 mathcomp/ssrtest/typeof.v delete mode 100644 mathcomp/ssrtest/unfold_Opaque.v delete mode 100644 mathcomp/ssrtest/unkeyed.v delete mode 100644 mathcomp/ssrtest/view_case.v delete mode 100644 mathcomp/ssrtest/wlog_suff.v delete mode 100644 mathcomp/ssrtest/wlogletin.v delete mode 100644 mathcomp/ssrtest/wlong_intro.v (limited to 'mathcomp') diff --git a/mathcomp/Make b/mathcomp/Make index 1db29ba..ee016ce 100644 --- a/mathcomp/Make +++ b/mathcomp/Make @@ -132,52 +132,6 @@ ssreflect/ssrnat.v ssreflect/ssrnotations.v ssreflect/ssrmatching.v ssreflect/tuple.v -ssrtest/absevarprop.v -ssrtest/abstract_var2.v -ssrtest/binders_of.v -ssrtest/binders.v -ssrtest/caseview.v -ssrtest/congr.v -ssrtest/deferclear.v -ssrtest/derive_inversion.v -ssrtest/dependent_type_err.v -ssrtest/elim2.v -ssrtest/elim_pattern.v -ssrtest/elim.v -ssrtest/explain_match.v -ssrtest/first_n.v -ssrtest/gen_have.v -ssrtest/gen_pattern.v -ssrtest/havesuff.v -ssrtest/have_TC.v -ssrtest/have_transp.v -ssrtest/have_view_idiom.v -ssrtest/if_isnt.v -ssrtest/indetLHS.v -ssrtest/intro_beta.v -ssrtest/intro_noop.v -ssrtest/ipatalternation.v -ssrtest/ltac_have.v -ssrtest/ltac_in.v -ssrtest/move_after.v -ssrtest/multiview.v -ssrtest/occarrow.v -ssrtest/patnoX.v -ssrtest/primproj.v -ssrtest/rewpatterns.v -ssrtest/set_lamda.v -ssrtest/set_pattern.v -ssrtest/ssrsyntax1.v -ssrtest/ssrsyntax2.v -ssrtest/tc.v -ssrtest/testmx.v -ssrtest/typeof.v -ssrtest/unfold_Opaque.v -ssrtest/unkeyed.v -ssrtest/view_case.v -ssrtest/wlogletin.v -ssrtest/wlog_suff.v -ssrtest/wlong_intro.v -I . -R . mathcomp diff --git a/mathcomp/ssrtest/Make b/mathcomp/ssrtest/Make deleted file mode 100644 index 836e12a..0000000 --- a/mathcomp/ssrtest/Make +++ /dev/null @@ -1,46 +0,0 @@ -absevarprop.v -binders_of.v -binders.v -caseview.v -congr.v -deferclear.v -dependent_type_err.v -elim2.v -elim_pattern.v -elim.v -first_n.v -gen_have.v -gen_pattern.v -havesuff.v -have_TC.v -have_transp.v -have_view_idiom.v -if_isnt.v -indetLHS.v -intro_beta.v -intro_noop.v -ipatalternation.v -ltac_have.v -ltac_in.v -move_after.v -multiview.v -occarrow.v -patnoX.v -primproj.v -rewpatterns.v -set_lamda.v -set_pattern.v -ssrsyntax1.v -ssrsyntax2.v -tc.v -testmx.v -typeof.v -unkeyed.v -unfold_Opaque.v -view_case.v -wlogletin.v -wlog_suff.v -wlong_intro.v - --R ../theories Ssreflect --I ../src/ diff --git a/mathcomp/ssrtest/Makefile b/mathcomp/ssrtest/Makefile deleted file mode 100644 index 14acb5c..0000000 --- a/mathcomp/ssrtest/Makefile +++ /dev/null @@ -1,25 +0,0 @@ -H=@ - -ifeq "$(COQBIN)" "" -COQBIN=$(dir $(shell which coqtop))/ -endif - -COQDEP=$(COQBIN)/coqdep - -OLD_MAKEFLAGS:=$(MAKEFLAGS) -MAKEFLAGS+=-B - -.DEFAULT_GOAL := all - -%: - $(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq - $(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \ - -f Makefile.coq $* \ - COQDEP='$(COQDEP) -c' - -.PHONY: clean -clean: - $(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \ - -f Makefile.coq clean - $(H)rm -f Makefile.coq - diff --git a/mathcomp/ssrtest/absevarprop.v b/mathcomp/ssrtest/absevarprop.v deleted file mode 100644 index e43f0f7..0000000 --- a/mathcomp/ssrtest/absevarprop.v +++ /dev/null @@ -1,90 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrfun eqtype ssrnat seq. -From mathcomp -Require Import fintype. - -Lemma test15: forall (y : nat) (x : 'I_2), y < 1 -> val x = y -> Some x = insub y. -move=> y x le_1 defx; rewrite insubT ?(leq_trans le_1) // => ?. -by congr (Some _); apply: val_inj=> /=; exact: defx. -Qed. - -Axiom P : nat -> Prop. -Axiom Q : forall n, P n -> Prop. -Definition R := fun (x : nat) (p : P x) m (q : P (x+1)) => m > 0. - -Inductive myEx : Type := ExI : forall n (pn : P n) pn', Q n pn -> R n pn n pn' -> myEx. - -Variable P1 : P 1. -Variable P11 : P (1 + 1). -Variable Q1 : forall P1, Q 1 P1. - -Lemma testmE1 : myEx. -Proof. -apply: ExI 1 _ _ _ _. - match goal with |- P 1 => exact: P1 | _ => fail end. - match goal with |- P (1+1) => exact: P11 | _ => fail end. - match goal with |- forall p : P 1, Q 1 p => move=> *; exact: Q1 | _ => fail end. -match goal with |- forall (p : P 1) (q : P (1+1)), is_true (R 1 p 1 q) => done | _ => fail end. -Qed. - -Lemma testE2 : exists y : { x | P x }, sval y = 1. -Proof. -apply: ex_intro (exist _ 1 _) _. - match goal with |- P 1 => exact: P1 | _ => fail end. -match goal with |- forall p : P 1, @sval _ _ (@exist _ _ 1 p) = 1 => done | _ => fail end. -Qed. - -Lemma testE3 : exists y : { x | P x }, sval y = 1. -Proof. -have := (ex_intro _ (exist _ 1 _) _); apply. - match goal with |- P 1 => exact: P1 | _ => fail end. -match goal with |- forall p : P 1, @sval _ _ (@exist _ _ 1 p) = 1 => done | _ => fail end. -Qed. - -Lemma testE4 : P 2 -> exists y : { x | P x }, sval y = 2. -Proof. -move=> P2; apply: ex_intro (exist _ 2 _) _. -match goal with |- @sval _ _ (@exist _ _ 2 P2) = 2 => done | _ => fail end. -Qed. - -Hint Resolve P1. - -Lemma testmE12 : myEx. -Proof. -apply: ExI 1 _ _ _ _. - match goal with |- P (1+1) => exact: P11 | _ => fail end. - match goal with |- Q 1 P1 => exact: Q1 | _ => fail end. -match goal with |- forall (q : P (1+1)), is_true (R 1 P1 1 q) => done | _ => fail end. -Qed. - -Create HintDb SSR. - -Hint Resolve P11 : SSR. - -Ltac ssrautoprop := trivial with SSR. - -Lemma testmE13 : myEx. -Proof. -apply: ExI 1 _ _ _ _. - match goal with |- Q 1 P1 => exact: Q1 | _ => fail end. -match goal with |- is_true (R 1 P1 1 P11) => done | _ => fail end. -Qed. - -Definition R1 := fun (x : nat) (p : P x) m (q : P (x+1)) (r : Q x p) => m > 0. - -Inductive myEx1 : Type := - ExI1 : forall n (pn : P n) pn' (q : Q n pn), R1 n pn n pn' q -> myEx1. - -Hint Resolve (Q1 P1) : SSR. - -(* tests that goals in prop are solved in the right order, propagating instantiations, - thus the goal Q 1 ?p1 is faced by trivial after ?p1, and is thus evar free *) -Lemma testmE14 : myEx1. -Proof. -apply: ExI1 1 _ _ _ _. -match goal with |- is_true (R1 1 P1 1 P11 (Q1 P1)) => done | _ => fail end. -Qed. - diff --git a/mathcomp/ssrtest/abstract_var2.v b/mathcomp/ssrtest/abstract_var2.v deleted file mode 100644 index 5372c5c..0000000 --- a/mathcomp/ssrtest/abstract_var2.v +++ /dev/null @@ -1,16 +0,0 @@ -Require Import ssreflect. - -Set Implicit Arguments. - -Axiom P : nat -> nat -> Prop. - -Axiom tr : - forall x y z, P x y -> P y z -> P x z. - -Lemma test a b c : P a c -> P a b. -Proof. -intro H. -Fail have [: s1 s2] H1 : P a b := @tr _ _ _ s1 s2. -have [: w s1 s2] H1 : P a b := @tr _ w _ s1 s2. -Abort. - diff --git a/mathcomp/ssrtest/binders.v b/mathcomp/ssrtest/binders.v deleted file mode 100644 index 32e351f..0000000 --- a/mathcomp/ssrtest/binders.v +++ /dev/null @@ -1,46 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool eqtype ssrnat. - -Lemma test (x : bool) : True. -have H1 x := x. -have (x) := x => H2. -have H3 T (x : T) := x. -have ? : bool := H1 _ x. -have ? : bool := H2 _ x. -have ? : bool := H3 _ x. -have ? (z : bool) : forall y : bool, z = z := fun y => refl_equal _. -have ? w : w = w := @refl_equal nat w. -have ? y : true by []. -have ? (z : bool) : z = z. - exact: (@refl_equal _ z). -have ? (z w : bool) : z = z by exact: (@refl_equal _ z). -have H w (a := 3) (_ := 4) : w && true = w. - by rewrite andbT. -exact I. -Qed. - -Lemma test1 : True. -suff (x : bool): x = x /\ True. - by move/(_ true); case=> _. -split; first by exact: (@refl_equal _ x). -suff H y : y && true = y /\ True. - by case: (H true). -suff H1 /= : true && true /\ True. - by rewrite andbT; split; [exact: (@refl_equal _ y) | exact: I]. -match goal with |- is_true true /\ True => idtac end. -by split. -Qed. - -Lemma foo n : n >= 0. -have f i (j := i + n) : j < n. - match goal with j := i + n |- _ => idtac end. -Undo 2. -suff f i (j := i + n) : j < n. - done. -match goal with j := i + n |- _ => idtac end. -Undo 3. -done. -Qed. diff --git a/mathcomp/ssrtest/binders_of.v b/mathcomp/ssrtest/binders_of.v deleted file mode 100644 index 2a88502..0000000 --- a/mathcomp/ssrtest/binders_of.v +++ /dev/null @@ -1,14 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) - -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import seq. - -Lemma test1 : True. -have f of seq nat & nat : nat. - exact 3. -have g of nat := 3. -have h of nat : nat := 3. -have _ : f [::] 3 = g 3 + h 4. -Admitted. diff --git a/mathcomp/ssrtest/caseview.v b/mathcomp/ssrtest/caseview.v deleted file mode 100644 index 478f573..0000000 --- a/mathcomp/ssrtest/caseview.v +++ /dev/null @@ -1,7 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. - - -Lemma test (A B : Prop) : A /\ B -> True. -Proof. by case=> _ /id _. Qed. \ No newline at end of file diff --git a/mathcomp/ssrtest/congr.v b/mathcomp/ssrtest/congr.v deleted file mode 100644 index 2a7b824..0000000 --- a/mathcomp/ssrtest/congr.v +++ /dev/null @@ -1,26 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool eqtype ssrnat. - -Lemma test1 : forall a b : nat, a == b -> a == 0 -> b == 0. -Proof. move=> a b Eab Eac; congr (_ == 0) : Eac; exact: eqP Eab. Qed. - -Definition arrow A B := A -> B. - -Lemma test2 : forall a b : nat, a == b -> arrow (a == 0) (b == 0). -Proof. move=> a b Eab; congr (_ == 0); exact: eqP Eab. Qed. - -Definition equals T (A B : T) := A = B. - -Lemma test3 : forall a b : nat, a = b -> equals nat (a + b) (b + b). -Proof. move=> a b E; congr (_ + _); exact E. Qed. - -Variable S : eqType. -Variable f : nat -> S. -Coercion f : nat >-> Equality.sort. - -Lemma test4 : forall a b : nat, b = a -> @eq S (b + b) (a + a). -Proof. move=> a b Eba; congr (_ + _); exact: Eba. Qed. - diff --git a/mathcomp/ssrtest/deferclear.v b/mathcomp/ssrtest/deferclear.v deleted file mode 100644 index 849a7c9..0000000 --- a/mathcomp/ssrtest/deferclear.v +++ /dev/null @@ -1,29 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. - -From mathcomp -Require Import ssrbool eqtype fintype ssrnat. - -Variable T : Type. - -Lemma test0 : forall a b c d : T, True. -Proof. by move=> a b {a} a c; exact I. Qed. - -Variable P : T -> Prop. - -Lemma test1 : forall a b c : T, P a -> forall d : T, True. -Proof. move=> a b {a} a _ d; exact I. Qed. - -Definition Q := forall x y : nat, x = y. -Axiom L : 0 = 0 -> Q. -Axiom L' : 0 = 0 -> forall x y : nat, x = y. -Lemma test3 : Q. -by apply/L. -Undo. -rewrite /Q. -by apply/L. -Undo 2. -by apply/L'. -Qed. - diff --git a/mathcomp/ssrtest/dependent_type_err.v b/mathcomp/ssrtest/dependent_type_err.v deleted file mode 100644 index ef2dc9d..0000000 --- a/mathcomp/ssrtest/dependent_type_err.v +++ /dev/null @@ -1,11 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrfun ssrbool eqtype ssrnat. - -Lemma ltn_leq_trans : forall n m p : nat, m < n -> n <= p -> m < p. -move=> n m p Hmn Hnp; rewrite -ltnS. -Fail rewrite (_ : forall n0 m0 p0 : nat, m0 <= n0 -> n0 < p0 -> m0 < p0). -Fail rewrite leq_ltn_trans. -Admitted. \ No newline at end of file diff --git a/mathcomp/ssrtest/derive_inversion.v b/mathcomp/ssrtest/derive_inversion.v deleted file mode 100644 index 0a344b8..0000000 --- a/mathcomp/ssrtest/derive_inversion.v +++ /dev/null @@ -1,19 +0,0 @@ -Require Import ssreflect ssrbool. - -Set Implicit Arguments. - - Inductive wf T : bool -> option T -> Type := - | wf_f : wf false None - | wf_t : forall x, wf true (Some x). - - Derive Inversion wf_inv with (forall T b (o : option T), wf b o) Sort Prop. - - Lemma Problem T b (o : option T) : - wf b o -> - match b with - | true => exists x, o = Some x - | false => o = None - end. - Proof. - by case: b; elim/wf_inv=> //; case: o=> // a *; exists a. - Qed. diff --git a/mathcomp/ssrtest/elim.v b/mathcomp/ssrtest/elim.v deleted file mode 100644 index 0a7b777..0000000 --- a/mathcomp/ssrtest/elim.v +++ /dev/null @@ -1,297 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrfun eqtype ssrnat seq. -Axiom daemon : False. Ltac myadmit := case: daemon. - -(* Ltac debugging feature: recursive elim + eq generation *) -Lemma testL1 : forall A (s : seq A), s = s. -Proof. -move=> A s; elim branch: s => [|x xs _]. -match goal with _ : _ = [::] |- [::] = [::] => move: branch => // | _ => fail end. -match goal with _ : _ = _ :: _ |- _ :: _ = _ :: _ => move: branch => // | _ => fail end. -Qed. - -(* The same but with explicit eliminator and a conflict in the intro pattern *) -Lemma testL2 : forall A (s : seq A), s = s. -Proof. -move=> A s; elim/last_ind branch: s => [|x s _]. -match goal with _ : _ = [::] |- [::] = [::] => move: branch => // | _ => fail end. -match goal with _ : _ = rcons _ _ |- rcons _ _ = rcons _ _ => move: branch => // | _ => fail end. -Qed. - -(* The same but without names for variables involved in the generated eq *) -Lemma testL3 : forall A (s : seq A), s = s. -Proof. -move=> A s; elim branch: s; move: (s) => _. -match goal with _ : _ = [::] |- [::] = [::] => move: branch => // | _ => fail end. -move=> _; match goal with _ : _ = _ :: _ |- _ :: _ = _ :: _ => move: branch => // | _ => fail end. -Qed. - -Inductive foo : Type := K1 : foo | K2 : foo -> foo -> foo | K3 : (nat -> foo) -> foo. - -(* The same but with more intros to be done *) -Lemma testL4 : forall (o : foo), o = o. -Proof. -move=> o; elim branch: o. -match goal with _ : _ = K1 |- K1 = K1 => move: branch => // | _ => fail end. -move=> _; match goal with _ : _ = K2 _ _ |- K2 _ _ = K2 _ _ => move: branch => // | _ => fail end. -move=> _; match goal with _ : _ = K3 _ |- K3 _ = K3 _ => move: branch => // | _ => fail end. -Qed. - -(* Occurrence counting *) -Lemma testO1: forall (b : bool), b = b. -Proof. -move=> b; case: (b) / idP. -match goal with |- is_true b -> true = true => done | _ => fail end. -match goal with |- ~ is_true b -> false = false => done | _ => fail end. -Qed. - -(* The same but only the second occ *) -Lemma testO2: forall (b : bool), b = b. -Proof. -move=> b; case: {2}(b) / idP. -match goal with |- is_true b -> b = true => done | _ => fail end. -match goal with |- ~ is_true b -> b = false => move/(introF idP) => // | _ => fail end. -Qed. - -(* The same but with eq generation *) -Lemma testO3: forall (b : bool), b = b. -Proof. -move=> b; case E: {2}(b) / idP. -match goal with _ : is_true b, _ : b = true |- b = true => move: E => _; done | _ => fail end. -match goal with H : ~ is_true b, _ : b = false |- b = false => move: E => _; move/(introF idP): H => // | _ => fail end. -Qed. - -(* Views *) -Lemma testV1 : forall A (s : seq A), s = s. -Proof. -move=> A s; case/lastP E: {1}s => [| x xs]. -match goal with _ : s = [::] |- [::] = s => symmetry; exact E | _ => fail end. -match goal with _ : s = rcons x xs |- rcons _ _ = s => symmetry; exact E | _ => fail end. -Qed. - -Lemma testV2 : forall A (s : seq A), s = s. -Proof. -move=> A s; case/lastP E: s => [| x xs]. -match goal with _ : s = [::] |- [::] = [::] => done | _ => fail end. -match goal with _ : s = rcons x xs |- rcons _ _ = rcons _ _ => done | _ => fail end. -Qed. - -Lemma testV3 : forall A (s : seq A), s = s. -Proof. -move=> A s; case/lastP: s => [| x xs]. -match goal with |- [::] = [::] => done | _ => fail end. -match goal with |- rcons _ _ = rcons _ _ => done | _ => fail end. -Qed. - -(* Patterns *) -Lemma testP1: forall (x y : nat), (y == x) && (y == x) -> y == x. -move=> x y; elim: {2}(_ == _) / eqP. -match goal with |- (y = x -> is_true ((y == x) && true) -> is_true (y == x)) => move=> -> // | _ => fail end. -match goal with |- (y <> x -> is_true ((y == x) && false) -> is_true (y == x)) => move=> _; rewrite andbC // | _ => fail end. -Qed. - -(* The same but with an implicit pattern *) -Lemma testP2 : forall (x y : nat), (y == x) && (y == x) -> y == x. -move=> x y; elim: {2}_ / eqP. -match goal with |- (y = x -> is_true ((y == x) && true) -> is_true (y == x)) => move=> -> // | _ => fail end. -match goal with |- (y <> x -> is_true ((y == x) && false) -> is_true (y == x)) => move=> _; rewrite andbC // | _ => fail end. -Qed. - -(* The same but with an eq generation switch *) -Lemma testP3 : forall (x y : nat), (y == x) && (y == x) -> y == x. -move=> x y; elim E: {2}_ / eqP. -match goal with _ : y = x |- (is_true ((y == x) && true) -> is_true (y == x)) => rewrite E; reflexivity | _ => fail end. -match goal with _ : y <> x |- (is_true ((y == x) && false) -> is_true (y == x)) => rewrite E => /= H; exact H | _ => fail end. -Qed. - -Inductive spec : nat -> nat -> nat -> Prop := -| specK : forall a b c, a = 0 -> b = 2 -> c = 4 -> spec a b c. -Lemma specP : spec 0 2 4. Proof. by constructor. Qed. - -Lemma testP4 : (1+1) * 4 = 2 + (1+1) + (2 + 2). -Proof. -case: specP => a b c defa defb defc. -match goal with |- (a.+1 + a.+1) * c = b + (a.+1 + a.+1) + (b + b) => subst; done | _ => fail end. -Qed. - -Lemma testP5 : (1+1) * 4 = 2 + (1+1) + (2 + 2). -Proof. -case: (1 + 1) _ / specP => a b c defa defb defc. -match goal with |- b * c = a.+2 + b + (a.+2 + a.+2) => subst; done | _ => fail end. -Qed. - -Lemma testP6 : (1+1) * 4 = 2 + (1+1) + (2 + 2). -Proof. -case: {2}(1 + 1) _ / specP => a b c defa defb defc. -match goal with |- (a.+1 + a.+1) * c = a.+2 + b + (a.+2 + a.+2) => subst; done | _ => fail end. -Qed. - -Lemma testP7 : (1+1) * 4 = 2 + (1+1) + (2 + 2). -Proof. -case: _ (1 + 1) (2 + _) / specP => a b c defa defb defc. -match goal with |- b * a.+4 = c + c => subst; done | _ => fail end. -Qed. - -Lemma testP8 : (1+1) * 4 = 2 + (1+1) + (2 + 2). -Proof. -case E: (1 + 1) (2 + _) / specP=> [a b c defa defb defc]. -match goal with |- b * a.+4 = c + c => subst; done | _ => fail end. -Qed. - -Variables (T : Type) (tr : T -> T). - -Inductive exec (cf0 cf1 : T) : seq T -> Prop := -| exec_step : tr cf0 = cf1 -> exec cf0 cf1 [::] -| exec_star : forall cf2 t, tr cf0 = cf2 -> - exec cf2 cf1 t -> exec cf0 cf1 (cf2 :: t). - -Inductive execr (cf0 cf1 : T) : seq T -> Prop := -| execr_step : tr cf0 = cf1 -> execr cf0 cf1 [::] -| execr_star : forall cf2 t, execr cf0 cf2 t -> - tr cf2 = cf1 -> execr cf0 cf1 (t ++ [:: cf2]). - -Lemma execP : forall cf0 cf1 t, exec cf0 cf1 t <-> execr cf0 cf1 t. -Proof. -move=> cf0 cf1 t; split => [] Ecf. - elim: Ecf. - match goal with |- forall cf2 cf3 : T, tr cf2 = cf3 -> - execr cf2 cf3 [::] => myadmit | _ => fail end. - match goal with |- forall (cf2 cf3 cf4 : T) (t0 : seq T), - tr cf2 = cf4 -> exec cf4 cf3 t0 -> execr cf4 cf3 t0 -> - execr cf2 cf3 (cf4 :: t0) => myadmit | _ => fail end. -elim: Ecf. - match goal with |- forall cf2 : T, - tr cf0 = cf2 -> exec cf0 cf2 [::] => myadmit | _ => fail end. -match goal with |- forall (cf2 cf3 : T) (t0 : seq T), - execr cf0 cf3 t0 -> exec cf0 cf3 t0 -> tr cf3 = cf2 -> - exec cf0 cf2 (t0 ++ [:: cf3]) => myadmit | _ => fail end. -Qed. - -From mathcomp -Require Import seq div prime bigop. - -Lemma mem_primes : forall p n, - (p \in primes n) = [&& prime p, n > 0 & p %| n]. -Proof. -move=> p n; rewrite andbCA; case: posnP => [-> // | /= n_gt0]. -apply/mapP/andP=> [[[q e]]|[pr_p]] /=. - case/mem_prime_decomp=> pr_q e_gt0; case/dvdnP=> u -> -> {p}. - by rewrite -(prednK e_gt0) expnS mulnCA dvdn_mulr. -rewrite {1}(prod_prime_decomp n_gt0) big_seq /=. -elim/big_ind: _ => [| u v IHu IHv | [q e] /= mem_qe dv_p_qe]. -- by rewrite Euclid_dvd1. -- by rewrite Euclid_dvdM //; case/orP. -exists (q, e) => //=; case/mem_prime_decomp: mem_qe => pr_q _ _. -by rewrite Euclid_dvdX // dvdn_prime2 // in dv_p_qe; case: eqP dv_p_qe. -Qed. - -Lemma sub_in_partn : forall pi1 pi2 n, - {in \pi(n), {subset pi1 <= pi2}} -> n`_pi1 %| n`_pi2. -Proof. -move=> pi1 pi2 n pi12; rewrite ![n`__]big_mkcond /=. -elim/big_ind2: _ => // [*|p _]; first exact: dvdn_mul. -rewrite lognE -mem_primes; case: ifP => pi1p; last exact: dvd1n. -by case: ifP => pr_p; [rewrite pi12 | rewrite if_same]. -Qed. - -Fixpoint plus (m n : nat) {struct n} : nat := - match n with - | 0 => m - | S p => S (plus m p) - end. - -Definition plus_equation : -forall m n : nat, - plus m n = - match n with - | 0 => m - | p.+1 => (plus m p).+1 - end -:= -fun m n : nat => -match - n as n0 - return - (forall m0 : nat, - plus m0 n0 = - match n0 with - | 0 => m0 - | p.+1 => (plus m0 p).+1 - end) -with -| 0 => @erefl nat -| n0.+1 => fun m0 : nat => erefl (plus m0 n0).+1 -end m. - -Definition plus_rect : -forall (m : nat) (P : nat -> nat -> Type), - (forall n : nat, n = 0 -> P 0 m) -> - (forall n p : nat, - n = p.+1 -> P p (plus m p) -> P p.+1 (plus m p).+1) -> - forall n : nat, P n (plus m n) -:= -fun (m : nat) (P : nat -> nat -> Type) - (f0 : forall n : nat, n = 0 -> P 0 m) - (f : forall n p : nat, - n = p.+1 -> P p (plus m p) -> P p.+1 (plus m p).+1) => -fix plus0 (n : nat) : P n (plus m n) := - eq_rect_r [eta P n] - (let f1 := f0 n in - let f2 := f n in - match - n as n0 - return - (n = n0 -> - (forall p : nat, - n0 = p.+1 -> P p (plus m p) -> P p.+1 (plus m p).+1) -> - (n0 = 0 -> P 0 m) -> - P n0 match n0 with - | 0 => m - | p.+1 => (plus m p).+1 - end) - with - | 0 => - fun (_ : n = 0) - (_ : forall p : nat, - 0 = p.+1 -> - P p (plus m p) -> P p.+1 (plus m p).+1) - (f4 : 0 = 0 -> P 0 m) => unkeyed (f4 (erefl 0)) - | n0.+1 => - fun (_ : n = n0.+1) - (f3 : forall p : nat, - n0.+1 = p.+1 -> - P p (plus m p) -> P p.+1 (plus m p).+1) - (_ : n0.+1 = 0 -> P 0 m) => - let f5 := - let p := n0 in - let H := erefl n0.+1 : n0.+1 = p.+1 in f3 p H in - unkeyed (let Hrec := plus0 n0 in f5 Hrec) - end (erefl n) f2 f1) (plus_equation m n). - -Definition plus_ind := plus_rect. - -Lemma exF x y z: plus (plus x y) z = plus x (plus y z). -elim/plus_ind: z / (plus _ z). -match goal with |- forall n : nat, n = 0 -> plus x y = plus x (plus y 0) => idtac end. -Undo 2. -elim/plus_ind: (plus _ z). -match goal with |- forall n : nat, n = 0 -> plus x y = plus x (plus y 0) => idtac end. -Undo 2. -elim/plus_ind: {z}(plus _ z). -match goal with |- forall n : nat, n = 0 -> plus x y = plus x (plus y 0) => idtac end. -Undo 2. -elim/plus_ind: {z}_. -match goal with |- forall n : nat, n = 0 -> plus x y = plus x (plus y 0) => idtac end. -Undo 2. -elim/plus_ind: z / _. -match goal with |- forall n : nat, n = 0 -> plus x y = plus x (plus y 0) => idtac end. - done. -by move=> _ p _ ->. -Qed. - -(* BUG elim-False *) -Lemma testeF : False -> 1 = 0. -Proof. by elim. Qed. diff --git a/mathcomp/ssrtest/elim2.v b/mathcomp/ssrtest/elim2.v deleted file mode 100644 index 4ba0b47..0000000 --- a/mathcomp/ssrtest/elim2.v +++ /dev/null @@ -1,63 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import eqtype ssrbool ssrnat seq div fintype finfun path bigop. -Axiom daemon : False. Ltac myadmit := case: daemon. - -Lemma big_load R (K K' : R -> Type) idx op I r (P : pred I) F : - let s := \big[op/idx]_(i <- r | P i) F i in - K s * K' s -> K' s. -Proof. by move=> /= [_]. Qed. -Arguments big_load [R] K [K' idx op I r P F]. - -Section Elim1. - -Variables (R : Type) (K : R -> Type) (f : R -> R). -Variables (idx : R) (op op' : R -> R -> R). - -Hypothesis Kid : K idx. - -Ltac ASSERT1 := match goal with |- (K idx) => myadmit end. -Ltac ASSERT2 K := match goal with |- (forall x1 : R, R -> - forall y1 : R, R -> K x1 -> K y1 -> K (op x1 y1)) => myadmit end. - - -Lemma big_rec I r (P : pred I) F - (Kop : forall i x, P i -> K x -> K (op (F i) x)) : - K (\big[op/idx]_(i <- r | P i) F i). -Proof. -elim/big_ind2: {-}_. - ASSERT1. ASSERT2 K. match goal with |- (forall i : I, is_true (P i) -> K (F i)) => myadmit end. Undo 4. -elim/big_ind2: _ / {-}_. - ASSERT1. ASSERT2 K. match goal with |- (forall i : I, is_true (P i) -> K (F i)) => myadmit end. Undo 4. - -elim/big_rec2: (\big[op/idx]_(i <- r | P i) op idx (F i)) - / (\big[op/idx]_(i <- r | P i) F i). - ASSERT1. match goal with |- (forall i : I, R -> forall y2 : R, is_true (P i) -> K y2 -> K (op (F i) y2)) => myadmit end. Undo 3. - -elim/(big_load (phantom R)): _. - Undo. - -Fail elim/big_rec2: {2}_. - -elim/big_rec2: (\big[op/idx]_(i <- r | P i) F i) - / {1}(\big[op/idx]_(i <- r | P i) F i). - Undo. - -elim/(big_load (phantom R)): _. -Undo. - -Fail elim/big_rec2: _ / {2}(\big[op/idx]_(i <- r | P i) F i). -Admitted. - -Definition morecomplexthannecessary A (P : A -> A -> Prop) x y := P x y. - -Lemma grab A (P : A -> A -> Prop) n m : (n = m) -> (P n n) -> morecomplexthannecessary A P n m. -by move->. -Qed. - -Goal forall n m, m + (n + m) = m + (n * 1 + m). -Proof. move=> n m; elim/grab : (_ * _) / {1}n => //; exact: muln1. Qed. - -End Elim1. diff --git a/mathcomp/ssrtest/elim_pattern.v b/mathcomp/ssrtest/elim_pattern.v deleted file mode 100644 index 24bd0fb..0000000 --- a/mathcomp/ssrtest/elim_pattern.v +++ /dev/null @@ -1,19 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool eqtype ssrnat. -Axiom daemon : False. Ltac myadmit := case: daemon. - -Lemma test x : (x == x) = (x + x.+1 == 2 * x + 1). -case: (X in _ = X) / eqP => _. -match goal with |- (x == x) = true => myadmit end. -match goal with |- (x == x) = false => myadmit end. -Qed. - -Lemma test1 x : (x == x) = (x + x.+1 == 2 * x + 1). -elim: (x in RHS). -match goal with |- (x == x) = _ => myadmit end. -match goal with |- forall n, (x == x) = _ -> (x == x) = _ => myadmit end. -Qed. - diff --git a/mathcomp/ssrtest/explain_match.v b/mathcomp/ssrtest/explain_match.v deleted file mode 100644 index 2c7bc2f..0000000 --- a/mathcomp/ssrtest/explain_match.v +++ /dev/null @@ -1,13 +0,0 @@ -Require Import ssrmatching. -Require Import ssreflect ssrbool ssrnat. - -Definition addnAC := (addnA, addnC). - -Lemma test x y z : x + y + z = x + y. - -ssrinstancesoftpat (_ + _). -ssrinstancesofruleL2R addnC. -ssrinstancesofruleR2L addnA. -ssrinstancesofruleR2L addnAC. -Fail ssrinstancesoftpat (_ + _ in RHS). (* Not implemented *) -Admitted. diff --git a/mathcomp/ssrtest/first_n.v b/mathcomp/ssrtest/first_n.v deleted file mode 100644 index 126f8a5..0000000 --- a/mathcomp/ssrtest/first_n.v +++ /dev/null @@ -1,12 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool. - -Lemma test : False -> (bool -> False -> True -> True) -> True. -move=> F; let w := constr:(2) in apply; last w first. -- by apply: F. -- by apply: I. -by apply: true. -Qed. \ No newline at end of file diff --git a/mathcomp/ssrtest/gen_have.v b/mathcomp/ssrtest/gen_have.v deleted file mode 100644 index d08cabe..0000000 --- a/mathcomp/ssrtest/gen_have.v +++ /dev/null @@ -1,165 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrfun ssrbool eqtype ssrnat. -Axiom daemon : False. Ltac myadmit := case: daemon. - -Axiom P : nat -> Prop. -Lemma clear_test (b1 b2 : bool) : b2 = b2. -Proof. -(* wlog gH : (b3 := b2) / b2 = b3. myadmit. *) -gen have {b1} H, gH : (b3 := b2) (w := erefl 3) / b2 = b3. - myadmit. -Fail exact (H b1). -exact (H b2 (erefl _)). -Qed. - - -Lemma test1 n (ngt0 : 0 < n) : P n. -gen have lt2le, /andP[H1 H2] : n ngt0 / (0 <= n) && (n != 0). - match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end. -Check (lt2le : forall n : nat, 0 < n -> (0 <= n) && (n != 0)). -Check (H1 : 0 <= n). -Check (H2 : n != 0). -myadmit. -Qed. - -Lemma test2 n (ngt0 : 0 < n) : P n. -gen have _, /andP[H1 H2] : n ngt0 / (0 <= n) && (n != 0). - match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end. -lazymatch goal with - | lt2le : forall n : nat, is_true(0 < n) -> is_true((0 <= n) && (n != 0)) - |- _ => fail "not cleared" - | _ => idtac end. -Check (H1 : 0 <= n). -Check (H2 : n != 0). -myadmit. -Qed. - -Lemma test3 n (ngt0 : 0 < n) : P n. -gen have H : n ngt0 / (0 <= n) && (n != 0). - match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end. -Check (H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)). -myadmit. -Qed. - -Lemma test4 n (ngt0 : 0 < n) : P n. -gen have : n ngt0 / (0 <= n) && (n != 0). - match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end. -move=> H. -Check(H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)). -myadmit. -Qed. - -Lemma test4bis n (ngt0 : 0 < n) : P n. -wlog suff : n ngt0 / (0 <= n) && (n != 0); last first. - match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end. -move=> H. -Check(H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)). -myadmit. -Qed. - -Lemma test5 n (ngt0 : 0 < n) : P n. -Fail gen have : / (0 <= n) && (n != 0). -Abort. - -Lemma test6 n (ngt0 : 0 < n) : P n. -gen have : n ngt0 / (0 <= n) && (n != 0) by myadmit. -Abort. - -Lemma test7 n (ngt0 : 0 < n) : P n. -Fail gen have : n / (0 <= n) && (n != 0). -Abort. - -Lemma test3wlog2 n (ngt0 : 0 < n) : P n. -gen have H : (m := n) ngt0 / (0 <= m) && (m != 0). - match goal with - ngt0 : is_true(0 < m) |- is_true((0 <= m) && (m != 0)) => myadmit end. -Check (H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)). -myadmit. -Qed. - -Lemma test3wlog3 n (ngt0 : 0 < n) : P n. -gen have H : {n} (m := n) (n := 0) ngt0 / (0 <= m) && (m != n). - match goal with - ngt0 : is_true(n < m) |- is_true((0 <= m) && (m != n)) => myadmit end. -Check (H : forall m n : nat, n < m -> (0 <= m) && (m != n)). -myadmit. -Qed. - -Lemma testw1 n (ngt0 : 0 < n) : n <= 0. -wlog H : (z := 0) (m := n) ngt0 / m != 0. - match goal with - |- (forall z m, - is_true(z < m) -> is_true(m != 0) -> is_true(m <= z)) -> - is_true(n <= 0) => myadmit end. -Check(n : nat). -Check(m : nat). -Check(z : nat). -Check(ngt0 : z < m). -Check(H : m != 0). -myadmit. -Qed. - -Lemma testw2 n (ngt0 : 0 < n) : n <= 0. -wlog H : (m := n) (z := (X in n <= X)) ngt0 / m != z. - match goal with - |- (forall m z : nat, - is_true(0 < m) -> is_true(m != z) -> is_true(m <= z)) -> - is_true(n <= 0) => idtac end. -Restart. -wlog H : (m := n) (one := (X in X <= _)) ngt0 / m != one. - match goal with - |- (forall m one : nat, - is_true(one <= m) -> is_true(m != one) -> is_true(m <= 0)) -> - is_true(n <= 0) => idtac end. -Restart. -wlog H : {n} (m := n) (z := (X in _ <= X)) ngt0 / m != z. - match goal with - |- (forall m z : nat, - is_true(0 < z) -> is_true(m != z) -> is_true(m <= 0)) -> - is_true(n <= 0) => idtac end. - myadmit. -Fail Check n. -myadmit. -Qed. - -Section Test. -Variable x : nat. -Definition addx y := y + x. - -Lemma testw3 (m n : nat) (ngt0 : 0 < n) : n <= addx x. -wlog H : (n0 := n) (y := x) (@twoy := (id _ as X in _ <= X)) / twoy = 2 * y. - myadmit. -myadmit. -Qed. - - -Definition twox := x + x. -Definition bis := twox. - -Lemma testw3x n (ngt0 : 0 < n) : n + x <= twox. -wlog H : (y := x) (@twoy := (X in _ <= X)) / twoy = 2 * y. - match goal with - |- (forall y : nat, - let twoy := y + y in - twoy = 2 * y -> is_true(n + y <= twoy)) -> - is_true(n + x <= twox) => myadmit end. -Restart. -wlog H : (y := x) (@twoy := (id _ as X in _ <= X)) / twoy = 2 * y. - match goal with - |- (forall y : nat, - let twoy := twox in - twoy = 2 * y -> is_true(n + y <= twoy)) -> - is_true(n + x <= twox) => myadmit end. -myadmit. -Qed. - -End Test. - -Lemma test_in n k (def_k : k = 0) (ngtk : k < n) : P n. -rewrite -(add0n n) in {def_k k ngtk} (m := k) (def_m := def_k) (ngtm := ngtk). -rewrite def_m add0n in {ngtm} (e := erefl 0 ) (ngt0 := ngtm) => {def_m}. -myadmit. -Qed. diff --git a/mathcomp/ssrtest/gen_pattern.v b/mathcomp/ssrtest/gen_pattern.v deleted file mode 100644 index eb4aee8..0000000 --- a/mathcomp/ssrtest/gen_pattern.v +++ /dev/null @@ -1,24 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrnat. - -Notation "( a 'in' c )" := (a + c) (only parsing) : myscope. -Delimit Scope myscope with myscope. - -Notation "( a 'in' c )" := (a + c) (only parsing). - -Lemma foo x y : x + x.+1 = x.+1 + y. -move: {x} (x.+1) {1}x y (x.+1 in RHS). - match goal with |- forall a b c d, b + a = d + c => idtac end. -Admitted. - -Lemma bar x y : x + x.+1 = x.+1 + y. -move E: ((x.+1 in y)) => w. - match goal with |- x + x.+1 = w => rewrite -{w}E end. -move E: (x.+1 in y)%myscope => w. - match goal with |- x + x.+1 = w => rewrite -{w}E end. -move E: ((x + y).+1 as RHS) => w. - match goal with |- x + x.+1 = w => rewrite -{}E -addSn end. -Admitted. \ No newline at end of file diff --git a/mathcomp/ssrtest/have_TC.v b/mathcomp/ssrtest/have_TC.v deleted file mode 100644 index c95b224..0000000 --- a/mathcomp/ssrtest/have_TC.v +++ /dev/null @@ -1,40 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. - -Axiom daemon : False. Ltac myadmit := case: daemon. - -Class foo (T : Type) := { n : nat }. -Instance five : foo nat := {| n := 5 |}. - -Definition bar T {f : foo T} m : Prop := - @n _ f = m. - -Eval compute in (bar nat 7). - -Lemma a : True. -set toto := bar _ 8. -have titi : bar _ 5. - reflexivity. -have titi2 : bar _ 5 := . - Fail reflexivity. - by myadmit. -have totoc (H : bar _ 5) : 3 = 3 := eq_refl. -move/totoc: nat => _. -exact I. -Qed. - -Set SsrHave NoTCResolution. - -Lemma a' : True. -set toto := bar _ 8. -have titi : bar _ 5. - Fail reflexivity. - by myadmit. -have titi2 : bar _ 5 := . - Fail reflexivity. - by myadmit. -have totoc (H : bar _ 5) : 3 = 3 := eq_refl. -move/totoc: nat => _. -exact I. -Qed. diff --git a/mathcomp/ssrtest/have_transp.v b/mathcomp/ssrtest/have_transp.v deleted file mode 100644 index 713f176..0000000 --- a/mathcomp/ssrtest/have_transp.v +++ /dev/null @@ -1,41 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype. - - -Lemma test1 n : n >= 0. -Proof. -have [:s1] @h m : 'I_(n+m).+1. - apply: Sub 0 _. - abstract: s1 m. - by auto. -cut (forall m, 0 < (n+m).+1); last assumption. -rewrite [_ 1 _]/= in s1 h *. -by []. -Qed. - -Lemma test2 n : n >= 0. -Proof. -have [:s1] @h m : 'I_(n+m).+1 := Sub 0 (s1 m). - move=> m; reflexivity. -cut (forall m, 0 < (n+m).+1); last assumption. -by []. -Qed. - -Lemma test3 n : n >= 0. -Proof. -Fail have [:s1] @h m : 'I_(n+m).+1 by apply: (Sub 0 (s1 m)); auto. -have [:s1] @h m : 'I_(n+m).+1 by apply: (Sub 0); abstract: s1 m; auto. -cut (forall m, 0 < (n+m).+1); last assumption. -by []. -Qed. - -Lemma test4 n : n >= 0. -Proof. -have @h m : 'I_(n+m).+1 by apply: (Sub 0); abstract auto. -by []. -Qed. - - diff --git a/mathcomp/ssrtest/have_view_idiom.v b/mathcomp/ssrtest/have_view_idiom.v deleted file mode 100644 index 07cfa11..0000000 --- a/mathcomp/ssrtest/have_view_idiom.v +++ /dev/null @@ -1,9 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool. - -Lemma test (a b : bool) (pab : a && b) : b. -have {pab} /= /andP [pa -> //] /= : true && (a && b) := pab. -Qed. diff --git a/mathcomp/ssrtest/havesuff.v b/mathcomp/ssrtest/havesuff.v deleted file mode 100644 index 4b0193a..0000000 --- a/mathcomp/ssrtest/havesuff.v +++ /dev/null @@ -1,75 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. - - -Variables P G : Prop. - -Lemma test1 : (P -> G) -> P -> G. -Proof. -move=> pg p. -have suff {pg} H : P. - match goal with |- P -> G => move=> _; exact: pg p | _ => fail end. -match goal with H : P -> G |- G => exact: H p | _ => fail end. -Qed. - -Lemma test2 : (P -> G) -> P -> G. -Proof. -move=> pg p. -have suffices {pg} H : P. - match goal with |- P -> G => move=> _; exact: pg p | _ => fail end. -match goal with H : P -> G |- G => exact: H p | _ => fail end. -Qed. - -Lemma test3 : (P -> G) -> P -> G. -Proof. -move=> pg p. -suff have {pg} H : P. - match goal with H : P |- G => exact: pg H | _ => fail end. -match goal with |- (P -> G) -> G => move=> H; exact: H p | _ => fail end. -Qed. - -Lemma test4 : (P -> G) -> P -> G. -Proof. -move=> pg p. -suffices have {pg} H: P. - match goal with H : P |- G => exact: pg H | _ => fail end. -match goal with |- (P -> G) -> G => move=> H; exact: H p | _ => fail end. -Qed. - -(* -Lemma test5 : (P -> G) -> P -> G. -Proof. -move=> pg p. -suff have {pg} H : P := pg H. -match goal with |- (P -> G) -> G => move=> H; exact: H p | _ => fail end. -Qed. -*) - -(* -Lemma test6 : (P -> G) -> P -> G. -Proof. -move=> pg p. -suff have {pg} H := pg H. -match goal with |- (P -> G) -> G => move=> H; exact: H p | _ => fail end. -Qed. -*) - -Lemma test7 : (P -> G) -> P -> G. -Proof. -move=> pg p. -have suff {pg} H : P := pg. -match goal with H : P -> G |- G => exact: H p | _ => fail end. -Qed. - -Lemma test8 : (P -> G) -> P -> G. -Proof. -move=> pg p. -have suff {pg} H := pg. -match goal with H : P -> G |- G => exact: H p | _ => fail end. -Qed. - -Goal forall x y : bool, x = y -> x = y. -move=> x y E. -by have {x E} -> : x = y by []. -Qed. \ No newline at end of file diff --git a/mathcomp/ssrtest/if_isnt.v b/mathcomp/ssrtest/if_isnt.v deleted file mode 100644 index 08e242e..0000000 --- a/mathcomp/ssrtest/if_isnt.v +++ /dev/null @@ -1,13 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. - - -Definition unopt (x : option bool) := - if x isn't Some x then false else x. - -Lemma test1 : unopt None = false /\ - unopt (Some false) = false /\ - unopt (Some true) = true. -Proof. by auto. Qed. - diff --git a/mathcomp/ssrtest/indetLHS.v b/mathcomp/ssrtest/indetLHS.v deleted file mode 100644 index edaf128..0000000 --- a/mathcomp/ssrtest/indetLHS.v +++ /dev/null @@ -1,8 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrnat. -Goal 5 = 3. -Fail (rewrite -(addnK _ 5)). -Abort. \ No newline at end of file diff --git a/mathcomp/ssrtest/intro_beta.v b/mathcomp/ssrtest/intro_beta.v deleted file mode 100644 index 4402be9..0000000 --- a/mathcomp/ssrtest/intro_beta.v +++ /dev/null @@ -1,15 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. - - -Axiom T : Type. - -Definition C (P : T -> Prop) := forall x, P x. - -Axiom P : T -> T -> Prop. - -Lemma foo : C (fun x => forall y, let z := x in P y x). -move=> a b. -match goal with |- (let y := _ in _) => idtac end. -Admitted. diff --git a/mathcomp/ssrtest/intro_noop.v b/mathcomp/ssrtest/intro_noop.v deleted file mode 100644 index 9b75bcf..0000000 --- a/mathcomp/ssrtest/intro_noop.v +++ /dev/null @@ -1,28 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool. -Axiom daemon : False. Ltac myadmit := case: daemon. - -Lemma v : True -> bool -> bool. Proof. by []. Qed. - -Reserved Notation " a -/ b " (at level 0). -Reserved Notation " a -// b " (at level 0). -Reserved Notation " a -/= b " (at level 0). -Reserved Notation " a -//= b " (at level 0). - -Lemma test : forall a b c, a || b || c. -Proof. -move=> ---a--- - -/=- -//- -/=- -//=- b [|-]. -move: {-}a => /v/v-H; have _ := H I I. -Fail move: {-}a {H} => /v-/v-H. -have - -> : a = (id a) by []. -have --> : a = (id a) by []. -have - - _ : a = (id a) by []. -have -{1}-> : a = (id a) by []. - by myadmit. -move: a. -case: b => -[] //. -by myadmit. -Qed. diff --git a/mathcomp/ssrtest/ipatalternation.v b/mathcomp/ssrtest/ipatalternation.v deleted file mode 100644 index 65f3760..0000000 --- a/mathcomp/ssrtest/ipatalternation.v +++ /dev/null @@ -1,8 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. - - -Lemma test1 : Prop -> Prop -> Prop -> Prop -> Prop -> True = False -> Prop -> True \/ True. -by move=> A /= /= /= B C {A} {B} ? _ {C} {1}-> *; right. -Qed. \ No newline at end of file diff --git a/mathcomp/ssrtest/ltac_have.v b/mathcomp/ssrtest/ltac_have.v deleted file mode 100644 index 1b30951..0000000 --- a/mathcomp/ssrtest/ltac_have.v +++ /dev/null @@ -1,32 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrnat. - -Ltac SUFF1 h t := suff h x (p := x < 0) : t. -Ltac SUFF2 h t := suff h x (p := x < 0) : t by apply h. -Ltac HAVE1 h t u := have h x (p := x < 0) : t := u. -Ltac HAVE2 h t := have h x (p := x < 0) : t by []. -Ltac HAVE3 h t := have h x (p := x < 0) : t. -Ltac HAVES h t := have suff h : t. -Ltac SUFFH h t := suff have h : t. - -Lemma foo z : z < 0. -SUFF1 h1 (z+1 < 0). -Undo. -SUFF2 h2 (z < 0). -Undo. -HAVE1 h3 (z = z) (refl_equal z). -Undo. -HAVE2 h4 (z = z). -Undo. -HAVE3 h5 (z < 0). -Undo. -HAVES h6 (z < 1). -Undo. -SUFFH h7 (z < 1). -Undo. -Admitted. - - diff --git a/mathcomp/ssrtest/ltac_in.v b/mathcomp/ssrtest/ltac_in.v deleted file mode 100644 index cec244d..0000000 --- a/mathcomp/ssrtest/ltac_in.v +++ /dev/null @@ -1,18 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool eqtype ssrnat ssrfun. - -Set Implicit Arguments. -Unset Strict Implicit. -Import Prenex Implicits. - -(* error 1 *) - -Ltac subst1 H := move: H; rewrite {1} addnC; move => H. -Ltac subst2 H := rewrite addnC in H. - -Goal ( forall a b: nat, b+a = 0 -> b+a=0). -Proof. move=> a b hyp. subst1 hyp. subst2 hyp. done. Qed. - diff --git a/mathcomp/ssrtest/move_after.v b/mathcomp/ssrtest/move_after.v deleted file mode 100644 index a6c455c..0000000 --- a/mathcomp/ssrtest/move_after.v +++ /dev/null @@ -1,9 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. - - -Goal True -> True -> True. -move=> H1 H2. -move H1 after H2. -Admitted. diff --git a/mathcomp/ssrtest/multiview.v b/mathcomp/ssrtest/multiview.v deleted file mode 100644 index 57a26ff..0000000 --- a/mathcomp/ssrtest/multiview.v +++ /dev/null @@ -1,60 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrnat. - -Goal forall m n p, n <= p -> m <= n -> m <= p. -by move=> m n p le_n_p /leq_trans; apply. -Undo 1. -by move=> m n p le_n_p /leq_trans /(_ le_n_p) le_m_p; exact: le_m_p. -Undo 1. -by move=> m n p le_n_p /leq_trans ->. -Qed. - -Goal forall P Q X : Prop, Q -> (True -> X -> Q = P) -> X -> P. -by move=> P Q X q V /V <-. -Qed. - -Lemma test0: forall a b, a && a && b -> b. -by move=> a b; repeat move=> /andP []; move=> *. -Qed. - -Lemma test1 : forall a b, a && b -> b. -by move=> a b /andP /andP /andP [] //. -Qed. - -Lemma test2 : forall a b, a && b -> b. -by move=> a b /andP /andP /(@andP a) [] //. -Qed. - -Lemma test3 : forall a b, a && (b && b) -> b. -by move=> a b /andP [_ /andP [_ //]]. -Qed. - -Lemma test4: forall a b, a && b = b && a. -by move=> a b; apply/andP/andP=> ?; apply/andP/andP/andP; rewrite andbC; apply/andP. -Qed. - -Lemma test5: forall C I A O, (True -> O) -> (O -> A) -> (True -> A -> I) -> (I -> C) -> C. -by move=> c i a o O A I C; apply/C/I/A/O. -Qed. - -Lemma test6: forall A B, (A -> B) -> A -> B. -move=> A B A_to_B a; move/A_to_B in a; exact: a. -Qed. - -Lemma test7: forall A B, (A -> B) -> A -> B. -move=> A B A_to_B a; apply A_to_B in a; exact: a. -Qed. - -From mathcomp -Require Import ssrfun eqtype ssrnat div seq choice fintype finfun finset. - -Lemma test8 (T : finType) (A B : {set T}) x (Ax : x \in A) (_ : B = A) : x \in B. -apply/subsetP: x Ax. -by rewrite H subxx. -Qed. - - - diff --git a/mathcomp/ssrtest/occarrow.v b/mathcomp/ssrtest/occarrow.v deleted file mode 100644 index 927473f..0000000 --- a/mathcomp/ssrtest/occarrow.v +++ /dev/null @@ -1,15 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import eqtype ssrnat. - -Lemma test1 : forall n m : nat, n = m -> m * m + n * n = n * n + n * n. -move=> n m E; have [{2}-> _] : n * n = m * n /\ True by move: E => {1}<-. -by move: E => {3}->. -Qed. - -Lemma test2 : forall n m : nat, True /\ (n = m -> n * n = n * m). -by move=> n m; constructor=> [|{2}->]. -Qed. - diff --git a/mathcomp/ssrtest/patnoX.v b/mathcomp/ssrtest/patnoX.v deleted file mode 100644 index a879b37..0000000 --- a/mathcomp/ssrtest/patnoX.v +++ /dev/null @@ -1,9 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool. -Goal forall x, x && true = x. -move=> x. -Fail (rewrite [X in _ && _]andbT). -Abort. diff --git a/mathcomp/ssrtest/primproj.v b/mathcomp/ssrtest/primproj.v deleted file mode 100644 index 05476fb..0000000 --- a/mathcomp/ssrtest/primproj.v +++ /dev/null @@ -1,157 +0,0 @@ - - -Require Import Setoid. -Set Primitive Projections. - - -Module CoqBug. -Record foo A := Foo { foo_car : A }. - -Definition bar : foo _ := Foo nat 10. - -Variable alias : forall A, foo A -> A. - -Parameter e : @foo_car = alias. - -Goal foo_car _ bar = alias _ bar. -Proof. -(* Coq equally fails *) -Fail rewrite -> e. -Fail rewrite e at 1. -Fail setoid_rewrite e. -Fail setoid_rewrite e at 1. -Set Keyed Unification. -Fail rewrite -> e. -Fail rewrite e at 1. -Fail setoid_rewrite e. -Fail setoid_rewrite e at 1. -Admitted. - -End CoqBug. - -(* ----------------------------------------------- *) - -From mathcomp Require Import ssreflect. - -Set Primitive Projections. - -Module T1. - -Record foo A := Foo { foo_car : A }. - -Definition bar : foo _ := Foo nat 10. - -Goal foo_car _ bar = 10. -Proof. -match goal with -| |- foo_car _ bar = 10 => idtac -end. -rewrite /foo_car. -(* -Fail match goal with -| |- foo_car _ bar = 10 => idtac -end. -*) -Admitted. - -End T1. - - -Module T2. - -Record foo {A} := Foo { foo_car : A }. - -Definition bar : foo := Foo nat 10. - -Goal foo_car bar = 10. -match goal with -| |- foo_car bar = 10 => idtac -end. -rewrite /foo_car. -(* -Fail match goal with -| |- foo_car bar = 10 => idtac -end. -*) -Admitted. - -End T2. - - -Module T3. - -Record foo {A} := Foo { foo_car : A }. - -Definition bar : foo := Foo nat 10. - -Goal foo_car bar = 10. -Proof. -rewrite -[foo_car _]/(id _). -match goal with |- id _ = 10 => idtac end. -Admitted. - -Goal foo_car bar = 10. -Proof. -set x := foo_car _. -match goal with |- x = 10 => idtac end. -Admitted. - -End T3. - -Module T4. - -Inductive seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }. -Arguments unseal {_ _} _. -Arguments seal_eq {_ _} _. - -Record uPred : Type := IProp { uPred_holds :> Prop }. - -Definition uPred_or_def (P Q : uPred) : uPred := - {| uPred_holds := P \/ Q |}. -Definition uPred_or_aux : seal (@uPred_or_def). by eexists. Qed. -Definition uPred_or := unseal uPred_or_aux. -Definition uPred_or_eq: @uPred_or = @uPred_or_def := seal_eq uPred_or_aux. - -Lemma foobar (P1 P2 Q : uPred) : - (P1 <-> P2) -> (uPred_or P1 Q) <-> (uPred_or P2 Q). -Proof. - rewrite uPred_or_eq. (* This fails. *) -Admitted. - -End T4. - - -Module DesignFlaw. - -Record foo A := Foo { foo_car : A }. -Definition bar : foo _ := Foo nat 10. - -Definition app (f : foo nat -> nat) x := f x. - -Goal app (foo_car _) bar = 10. -Proof. -unfold app. (* mkApp should produce a Proj *) -Fail set x := (foo_car _ _). -Admitted. - -End DesignFlaw. - - -Module Bug. - -Record foo A := Foo { foo_car : A }. - -Definition bar : foo _ := Foo nat 10. - -Variable alias : forall A, foo A -> A. - -Parameter e : @foo_car = alias. - -Goal foo_car _ bar = alias _ bar. -Proof. -Fail rewrite e. (* Issue: #86 *) -Admitted. - -End Bug. - - diff --git a/mathcomp/ssrtest/rewpatterns.v b/mathcomp/ssrtest/rewpatterns.v deleted file mode 100644 index 22ca265..0000000 --- a/mathcomp/ssrtest/rewpatterns.v +++ /dev/null @@ -1,181 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) - -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrfun eqtype ssrnat. - -Lemma test1 : forall x y (f : nat -> nat), f (x + y).+1 = f (y + x.+1). -by move=> x y f; rewrite [_.+1](addnC x.+1). -Qed. - -Lemma test2 : forall x y f, x + y + f (y + x) + f (y + x) = x + y + f (y + x) + f (x + y). -by move=> x y f; rewrite {2}[in f _]addnC. -Qed. - -Lemma test2' : forall x y f, true && f (x * (y + x)) = true && f(x * (x + y)). -by move=> x y f; rewrite [in f _](addnC y). -Qed. - -Lemma test2'' : forall x y f, f (y + x) + f(y + x) + f(y + x) = f(x + y) + f(y + x) + f(x + y). -by move=> x y f; rewrite {1 3}[in f _](addnC y). -Qed. - -(* patterns catching bound vars not supported *) -Lemma test2_1 : forall x y f, true && (let z := x in f (z * (y + x))) = true && f(x * (x + y)). -by move=> x y f; rewrite [in f _](addnC x). (* put y when bound var will be OK *) -Qed. - -Lemma test3 : forall x y f, x + f (x + y) (f (y + x) x) = x + f (x + y) (f (x + y) x). -by move=> x y f; rewrite [in X in (f _ X)](addnC y). -Qed. - -Lemma test3' : forall x y f, x = y -> x + f (x + x) x + f (x + x) x = - x + f (x + y) x + f (y + x) x. -by move=> x y f E; rewrite {2 3}[in X in (f X _)]E. -Qed. - -Lemma test3'' : forall x y f, x = y -> x + f (x + y) x + f (x + y) x = - x + f (x + y) x + f (y + y) x. -by move=> x y f E; rewrite {2}[in X in (f X _)]E. -Qed. - -Lemma test4 : forall x y f, x = y -> x + f (fun _ : nat => x + x) x + f (fun _ => x + x) x = - x + f (fun _ => x + y) x + f (fun _ => y + x) x. -by move=> x y f E; rewrite {2 3}[in X in (f X _)]E. -Qed. - -Lemma test4' : forall x y f, x = y -> x + f (fun _ _ _ : nat => x + x) x = - x + f (fun _ _ _ => x + y) x. -by move=> x y f E; rewrite {2}[in X in (f X _)]E. -Qed. - -Lemma test5 : forall x y f, x = y -> x + f (y + x) x + f (y + x) x = - x + f (x + y) x + f (y + x) x. -by move=> x y f E; rewrite {1}[X in (f X _)]addnC. -Qed. - -Lemma test3''' : forall x y f, x = y -> x + f (x + y) x + f (x + y) (x + y) = - x + f (x + y) x + f (y + y) (x + y). -by move=> x y f E; rewrite {1}[in X in (f X X)]E. -Qed. - -Lemma test3'''' : forall x y f, x = y -> x + f (x + y) x + f (x + y) (x + y) = - x + f (x + y) x + f (y + y) (y + y). -by move=> x y f E; rewrite [in X in (f X X)]E. -Qed. - -Lemma test3x : forall x y f, y+y = x+y -> x + f (x + y) x + f (x + y) (x + y) = - x + f (x + y) x + f (y + y) (y + y). -by move=> x y f E; rewrite -[X in (f X X)]E. -Qed. - -Lemma test6 : forall x y (f : nat -> nat), f (x + y).+1 = f (y.+1 + x). -by move=> x y f; rewrite [(x + y) in X in (f X)]addnC. -Qed. - -Lemma test7 : forall x y (f : nat -> nat), f (x + y).+1 = f (y + x.+1). -by move=> x y f; rewrite [(x.+1 + y) as X in (f X)]addnC. -Qed. - -Lemma manual x y z (f : nat -> nat -> nat) : (x + y).+1 + f (x.+1 + y) (z + (x + y).+1) = 0. -Proof. -rewrite [in f _]addSn. -match goal with |- (x + y).+1 + f (x + y).+1 (z + (x + y).+1) = 0 => idtac end. -rewrite -[X in _ = X]addn0. -match goal with |- (x + y).+1 + f (x + y).+1 (z + (x + y).+1) = 0 + 0 => idtac end. -rewrite -{2}[in X in _ = X](addn0 0). -match goal with |- (x + y).+1 + f (x + y).+1 (z + (x + y).+1) = 0 + (0 + 0) => idtac end. -rewrite [_.+1 in X in f _ X](addnC x.+1). -match goal with |- (x + y).+1 + f (x + y).+1 (z + (y + x.+1)) = 0 + (0 + 0) => idtac end. -rewrite [x.+1 + y as X in f X _]addnC. -match goal with |- (x + y).+1 + f (y + x.+1) (z + (y + x.+1)) = 0 + (0 + 0) => idtac end. -Admitted. - -From mathcomp -Require Import fintype ssrnat finset fingroup gproduct. - -Goal (forall (gT : finGroupType) (G H: {set gT}) (Z : {group gT}), G = Z). -move=> gT G H K. suff: G \x H = K. case/dprodP=> {G H} [[G H -> -> defK _ _]]. -Admitted. - -Goal (exists x : 'I_3, x > 0). -apply: (ex_intro _ (@Ordinal _ 2 _)). -Admitted. - -Goal (forall y, 1 < y < 2 -> exists x : 'I_3, x > 0). -move=> y; case/andP=> y_gt1 y_lt2; apply: (ex_intro _ (@Ordinal _ y _)). - by apply: leq_trans y_lt2 _. -by move=> y_lt3; apply: leq_trans _ y_gt1. -Qed. - -Goal (forall x y : nat, forall P : nat -> Prop, x = y -> True). -move=> x y P E. -have: P x -> P y by suff: x = y by move=> ?; congr (P _). -Admitted. - -Goal forall a : bool, a -> true && a || false && a. -by move=> a ?; rewrite [true && _]/= [_ && a]/= orbC [_ || _]//=. -Qed. - -Goal forall a : bool, a -> true && a || false && a. -by move=> a ?; rewrite [X in X || _]/= [X in _ || X]/= orbC [false && a as X in X || _]//=. -Qed. - -Variable a : bool. -Definition f x := x || a. -Definition g x := f x. - -Goal a -> g false. -by move=> Ha; rewrite [g _]/f orbC Ha. -Qed. - -Goal a -> g false || g false. -move=> Ha; rewrite {2}[g _]/f orbC Ha. -match goal with |- (is_true (false || true || g false)) => done end. -Qed. - -Goal a -> (a && a || true && a) && true. -by move=> Ha; rewrite -[_ || _]/(g _) andbC /= Ha [g _]/f. -Qed. - -Goal a -> (a || a) && true. -by move=> Ha; rewrite -[in _ || _]/(f _) Ha andbC /f. -Qed. - -(* -Lemma testM7: forall x y, 0 = x + y -> y = 0 -> x = 0 -> 0 = y + x. -move=> x y E H1 H2; rewrite -[x + y as X in _ = X]E. -*) -(* -Lemma testM7': forall x y, 0 = x + y -> y = 0 -> x = 0 -> 0 = y + x. -move=> x y E H1 H2; rewrite -[y + x as X in _ = X]E. -*) -(* -Lemma testM6: forall x y, 0 = x + y -> y = 0 -> x = 0 -> 0 = y + x. -move=> x y E H1 H2; rewrite -[y + x in X in _ = X]E. -*) -(* -Lemma testM6': forall x y, 0 = x + y -> y = 0 -> x = 0 -> 0 = y + x. -move=> x y E H1 H2; rewrite -[x + y in X in _ = X]E. -*) -(* -Lemma testM5: forall x y, 0 = x + y -> y = 0 -> x = 0 -> 0 = y + x. -move=> x y E H1 H2; rewrite -[in X in _ = X]E. -*) -(* -Lemma testM4: forall x y, 0 = x + y -> y = 0 -> x = 0 -> 0 = y + x. -move=> x y E H1 H2; rewrite -[X in _ = X]E. -*) -(* -Lemma testM3: forall x y, 0 = x + y -> y = 0 -> x = 0 -> 0 = y + x. -move=> x y E H1 H2; rewrite -[in _ = _]E. -*) -(* -Lemma testM2 : forall x y, 0 = x + y -> y = 0 -> x = 0 -> 0 = y + x. -move=> x y E H1 H2; rewrite -[x + y]E. -*) -(* -Lemma testM1 : forall x y, 0 = x + y -> y = 0 -> x = 0 -> 0 = y + x. -move=> x y E H1 H2; rewrite -E. -*) diff --git a/mathcomp/ssrtest/set_lamda.v b/mathcomp/ssrtest/set_lamda.v deleted file mode 100644 index 6366130..0000000 --- a/mathcomp/ssrtest/set_lamda.v +++ /dev/null @@ -1,18 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool eqtype ssrnat ssrfun. - -Set Implicit Arguments. -Unset Strict Implicit. -Import Prenex Implicits. - -(* error 2 *) - -Goal (exists f: Set -> nat, f nat = 0). -Proof. set (f:= fun _:Set =>0). by exists f. Qed. - -Goal (exists f: Set -> nat, f nat = 0). -Proof. set f := (fun _:Set =>0). by exists f. Qed. - diff --git a/mathcomp/ssrtest/set_pattern.v b/mathcomp/ssrtest/set_pattern.v deleted file mode 100644 index 5d22ef2..0000000 --- a/mathcomp/ssrtest/set_pattern.v +++ /dev/null @@ -1,57 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. - -Axiom daemon : False. Ltac myadmit := case: daemon. - -Ltac T1 x := match goal with |- _ => set t := (x in X in _ = X) end. -Ltac T2 x := first [set t := (x in RHS)]. -Ltac T3 x := first [set t := (x in Y in _ = Y)|idtac]. -Ltac T4 x := set t := (x in RHS); idtac. -Ltac T5 x := match goal with |- _ => set t := (x in RHS) | |- _ => idtac end. - -From mathcomp -Require Import ssrbool ssrnat. - -Lemma foo x y : x.+1 = y + x.+1. -set t := (_.+1 in RHS). match goal with |- x.+1 = y + t => rewrite /t {t} end. -set t := (x in RHS). match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end. -set t := (x in _ = x). match goal with |- x.+1 = t => rewrite /t {t} end. -set t := (x in X in _ = X). - match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end. -set t := (x in RHS). match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end. -set t := (y + (1 + x) as X in _ = X). - match goal with |- x.+1 = t => rewrite /t addSn add0n {t} end. -set t := x.+1. match goal with |- t = y + t => rewrite /t {t} end. -set t := (x).+1. match goal with |- t = y + t => rewrite /t {t} end. -set t := ((x).+1 in X in _ = X). - match goal with |- x.+1 = y + t => rewrite /t {t} end. -set t := (x.+1 in RHS). match goal with |- x.+1 = y + t => rewrite /t {t} end. -T1 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end. -T2 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end. -T3 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end. -T4 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end. -T5 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end. -rewrite [RHS]addnC. - match goal with |- x.+1 = x.+1 + y => rewrite -[RHS]addnC end. -rewrite -[in RHS](@subnK 1 x.+1) //. - match goal with |- x.+1 = y + (x.+1 - 1 + 1) => rewrite subnK // end. -have H : x.+1 = y by myadmit. -set t := _.+1 in H |- *. - match goal with H : t = y |- t = y + t => rewrite /t {t} in H * end. -set t := (_.+1 in X in _ + X) in H |- *. - match goal with H : x.+1 = y |- x.+1 = y + t => rewrite /t {t} in H * end. -set t := 0. match goal with t := 0 |- x.+1 = y + x.+1 => clear t end. -set t := y + _. match goal with |- x.+1 = t => rewrite /t {t} end. -set t : nat := 0. clear t. -set t : nat := (x in RHS). - match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end. -set t : nat := RHS. match goal with |- x.+1 = t => rewrite /t {t} end. -(* set t := 0 + _. *) -(* set t := (x).+1 in X in _ + X in H |-. *) -(* set t := (x).+1 in X in _ = X.*) -Admitted. - - - - diff --git a/mathcomp/ssrtest/ssrsyntax1.v b/mathcomp/ssrtest/ssrsyntax1.v deleted file mode 100644 index 3fc202f..0000000 --- a/mathcomp/ssrtest/ssrsyntax1.v +++ /dev/null @@ -1,26 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require mathcomp.ssreflect.ssreflect. -Require Import Arith. - -Goal (forall a b, a + b = b + a). -intros. -rewrite plus_comm, plus_comm. -split. -Abort. - -Module Foo. -Import ssreflect. - -Goal (forall a b, a + b = b + a). -intros. -rewrite 2![_ + _]plus_comm. -split. -Abort. -End Foo. - -Goal (forall a b, a + b = b + a). -intros. -rewrite plus_comm, plus_comm. -split. -Abort. \ No newline at end of file diff --git a/mathcomp/ssrtest/ssrsyntax2.v b/mathcomp/ssrtest/ssrsyntax2.v deleted file mode 100644 index 5e174a2..0000000 --- a/mathcomp/ssrtest/ssrsyntax2.v +++ /dev/null @@ -1,11 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssrtest.ssrsyntax1. -Require Import Arith. - -Goal (forall a b, a + b = b + a). -intros. -rewrite plus_comm, plus_comm. -split. -Qed. - diff --git a/mathcomp/ssrtest/tc.v b/mathcomp/ssrtest/tc.v deleted file mode 100644 index 20d190f..0000000 --- a/mathcomp/ssrtest/tc.v +++ /dev/null @@ -1,32 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. - - -Class foo (A : Type) : Type := mkFoo { val : A }. -Instance foo_pair {A B} {f1 : foo A} {f2 : foo B} : foo (A * B) | 2 := - {| val := (@val _ f1, @val _ f2) |}. -Instance foo_nat : foo nat | 3 := {| val := 0 |}. - -Definition id {A} (x : A) := x. -Axiom E : forall A {f : foo A} (a : A), id a = (@val _ f). - -Lemma test (x : nat) : id true = true -> id x = 0. -Proof. -Fail move=> _; reflexivity. -Timeout 2 rewrite E => _; reflexivity. -Qed. - -Definition P {A} (x : A) : Prop := x = x. -Axiom V : forall A {f : foo A} (x:A), P x -> P (id x). - -Lemma test1 (x : nat) : P x -> P (id x). -Proof. -move=> px. -Timeout 2 Fail move/V: px. -Timeout 2 move/V : (px) => _. -move/(V nat) : px => H; exact H. -Qed. - - - diff --git a/mathcomp/ssrtest/testmx.v b/mathcomp/ssrtest/testmx.v deleted file mode 100644 index 7d90d29..0000000 --- a/mathcomp/ssrtest/testmx.v +++ /dev/null @@ -1,37 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrfun ssrbool eqtype ssrnat. -From mathcomp -Require Import ssralg matrix. - -Set Implicit Arguments. -Unset Strict Implicit. -Import Prenex Implicits. - -Local Open Scope nat_scope. -Local Open Scope ring_scope. - -Section TestMx. - -Variable R : ringType. -Variable M : 'M[R]_2. - -Goal 1%:M = M. -Proof. -Set Printing All. -rewrite [(1%:M : 'M_(1+1)%N)]scalar_mx_block. -(* Success with 1.2 *) -(* With ssreflect 1.3, fails with error : *) -(* Toplevel input, characters 0-44: *) -(* Error: pattern (1%:M) does not match LHS of scalar_mx_block *) -Admitted. - -Goal 1%:M = M. -Proof. -rewrite [1%:M](scalar_mx_block 1%N 1%N). -(* Success in both ssr 1.2 and 1.3 *) -Admitted. - -End TestMx. \ No newline at end of file diff --git a/mathcomp/ssrtest/typeof.v b/mathcomp/ssrtest/typeof.v deleted file mode 100644 index f2cb1d4..0000000 --- a/mathcomp/ssrtest/typeof.v +++ /dev/null @@ -1,12 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. - -Ltac mycut x := - let tx := type of x in - cut tx. - -Lemma test : True. -Proof. -by mycut I=> [ x | ]; [ exact x | exact I ]. -Qed. \ No newline at end of file diff --git a/mathcomp/ssrtest/unfold_Opaque.v b/mathcomp/ssrtest/unfold_Opaque.v deleted file mode 100644 index 1ebcbe4..0000000 --- a/mathcomp/ssrtest/unfold_Opaque.v +++ /dev/null @@ -1,8 +0,0 @@ -Require Import ssreflect. - -Definition x := 3. -Opaque x. - -Goal x = 3. -Fail rewrite /x. -Admitted. \ No newline at end of file diff --git a/mathcomp/ssrtest/unkeyed.v b/mathcomp/ssrtest/unkeyed.v deleted file mode 100644 index 5ab6eba..0000000 --- a/mathcomp/ssrtest/unkeyed.v +++ /dev/null @@ -1,22 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrfun ssrbool eqtype. - -Set Implicit Arguments. -Unset Strict Implicit. -Import Prenex Implicits. - -Lemma test0 (a b : unit) f : a = f b. -Proof. by rewrite !unitE. Qed. - -Lemma phE T : all_equal_to (Phant T). Proof. by case. Qed. - -Lemma test1 (a b : phant nat) f : a = f b. -Proof. by rewrite !phE. Qed. - -Lemma eq_phE (T : eqType) : all_equal_to (Phant T). Proof. by case. Qed. - -Lemma test2 (a b : phant bool) f : a = locked (f b). -Proof. by rewrite !eq_phE. Qed. diff --git a/mathcomp/ssrtest/view_case.v b/mathcomp/ssrtest/view_case.v deleted file mode 100644 index e9104a9..0000000 --- a/mathcomp/ssrtest/view_case.v +++ /dev/null @@ -1,22 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrnat eqtype seq fintype zmodp. - -Axiom P : forall T, seq T -> Prop. - -Goal (forall T (s : seq T), P _ s). -move=> T s. -elim: s => [| x /lastP [| s] IH]. -Admitted. - -Goal forall x : 'I_1, x = 0 :> nat. -move=> /ord1 -> /=; exact: refl_equal. -Qed. - -Goal forall x : 'I_1, x = 0 :> nat. -move=> x. -move=> /ord1 -> in x |- *. -exact: refl_equal. -Qed. diff --git a/mathcomp/ssrtest/wlog_suff.v b/mathcomp/ssrtest/wlog_suff.v deleted file mode 100644 index bc931e1..0000000 --- a/mathcomp/ssrtest/wlog_suff.v +++ /dev/null @@ -1,19 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool. - -Lemma test b : b || ~~b. -wlog _ : b / b = true. - case: b; [ by apply | by rewrite orbC ]. -wlog suff: b / b || ~~b. - by case: b. -by case: b. -Qed. - -Lemma test2 b c (H : c = b) : b || ~~b. -wlog _ : b {c H} / b = true. - by case: b H. -by case: b. -Qed. \ No newline at end of file diff --git a/mathcomp/ssrtest/wlogletin.v b/mathcomp/ssrtest/wlogletin.v deleted file mode 100644 index faeca5c..0000000 --- a/mathcomp/ssrtest/wlogletin.v +++ /dev/null @@ -1,40 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import eqtype ssrbool. - -Variable T : Type. -Variables P : T -> Prop. - -Definition f := fun x y : T => x. - -Lemma test1 : forall x y : T, P (f x y) -> P x. -Proof. -move=> x y; set fxy := f x y; move=> Pfxy. -wlog H : @fxy Pfxy / P x. - match goal with |- (let fxy0 := f x y in P fxy0 -> P x -> P x) -> P x => by auto | _ => fail end. -exact: H. -Qed. - -Lemma test2 : forall x y : T, P (f x y) -> P x. -Proof. -move=> x y; set fxy := f x y; move=> Pfxy. -wlog H : fxy Pfxy / P x. - match goal with |- (forall fxy, P fxy -> P x -> P x) -> P x => by auto | _ => fail end. -exact: H. -Qed. - -Lemma test3 : forall x y : T, P (f x y) -> P x. -Proof. -move=> x y; set fxy := f x y; move=> Pfxy. -move: {1}@fxy (Pfxy) (Pfxy). -match goal with |- (let fxy0 := f x y in P fxy0 -> P fxy -> P x) => by auto | _ => fail end. -Qed. - -Lemma test4 : forall n m z: bool, n = z -> let x := n in x = m && n -> x = m && n. -move=> n m z E x H. -case: true. - by rewrite {1 2}E in (x) H |- *. -by rewrite {1}E in x H |- *. -Qed. diff --git a/mathcomp/ssrtest/wlong_intro.v b/mathcomp/ssrtest/wlong_intro.v deleted file mode 100644 index 836dd4b..0000000 --- a/mathcomp/ssrtest/wlong_intro.v +++ /dev/null @@ -1,10 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrnat. - -Goal (forall x y : nat, True). -move=> x y. -wlog suff: x y / x <= y. -Admitted. -- cgit v1.2.3