diff options
Diffstat (limited to 'mathcomp/ssrtest')
43 files changed, 1531 insertions, 0 deletions
diff --git a/mathcomp/ssrtest/Make b/mathcomp/ssrtest/Make new file mode 100644 index 0000000..adcc2d2 --- /dev/null +++ b/mathcomp/ssrtest/Make @@ -0,0 +1,44 @@ +-R ../theories Ssreflect +-I ../src/ +absevarprop.v +binders.v +binders_of.v +caseview.v +congr.v +deferclear.v +dependent_type_err.v +elim.v +elim2.v +elim_pattern.v +first_n.v +gen_pattern.v +gen_have.v +havesuff.v +have_view_idiom.v +have_TC.v +have_transp.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 +rewpatterns.v +set_lamda.v +set_pattern.v +ssrsyntax1.v +ssrsyntax2.v +testmx.v +tc.v +typeof.v +unkeyed.v +view_case.v +wlogletin.v +wlong_intro.v +wlog_suff.v + diff --git a/mathcomp/ssrtest/Makefile b/mathcomp/ssrtest/Makefile new file mode 100644 index 0000000..4bcf4fb --- /dev/null +++ b/mathcomp/ssrtest/Makefile @@ -0,0 +1,26 @@ +MAKEFLAGS := -r + +.SUFFIXES: + +.PHONY: clean all config tags install + +COQMAKEFILE := Makefile.coq +COQMAKE := +$(MAKE) -f $(COQMAKEFILE) + +all: $(COQMAKEFILE) + $(COQMAKE) all + +$(COQMAKEFILE) config: + $(COQBIN)coq_makefile -f Make -o $(COQMAKEFILE) + +clean: $(COQMAKEFILE) + $(COQMAKE) clean + $(RM) -rf $(COQMAKEFILE) + +tags: + $(COQBIN)coqtags `find . -name \*.v` + +install: + +%: Makefile.coq + $(COQMAKE) $@ diff --git a/mathcomp/ssrtest/absevarprop.v b/mathcomp/ssrtest/absevarprop.v new file mode 100644 index 0000000..513e53f --- /dev/null +++ b/mathcomp/ssrtest/absevarprop.v @@ -0,0 +1,86 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. +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/binders.v b/mathcomp/ssrtest/binders.v new file mode 100644 index 0000000..6a63167 --- /dev/null +++ b/mathcomp/ssrtest/binders.v @@ -0,0 +1,43 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect 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 new file mode 100644 index 0000000..70a822e --- /dev/null +++ b/mathcomp/ssrtest/binders_of.v @@ -0,0 +1,12 @@ + +Require Import ssreflect 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. + by admit. +by admit. +Qed.
\ No newline at end of file diff --git a/mathcomp/ssrtest/caseview.v b/mathcomp/ssrtest/caseview.v new file mode 100644 index 0000000..108cf46 --- /dev/null +++ b/mathcomp/ssrtest/caseview.v @@ -0,0 +1,4 @@ +Require Import 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 new file mode 100644 index 0000000..edd52fe --- /dev/null +++ b/mathcomp/ssrtest/congr.v @@ -0,0 +1,23 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect 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 new file mode 100644 index 0000000..a13a20e --- /dev/null +++ b/mathcomp/ssrtest/deferclear.v @@ -0,0 +1,26 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect. +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 new file mode 100644 index 0000000..cd9570b --- /dev/null +++ b/mathcomp/ssrtest/dependent_type_err.v @@ -0,0 +1,7 @@ +Require Import ssreflect 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/elim.v b/mathcomp/ssrtest/elim.v new file mode 100644 index 0000000..5ab8f41 --- /dev/null +++ b/mathcomp/ssrtest/elim.v @@ -0,0 +1,222 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. + +(* 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 [::] => admit | _ => 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) => admit | _ => fail end. +elim: Ecf. + match goal with |- forall cf2 : T, + tr cf0 = cf2 -> exec cf0 cf2 [::] => admit | _ => 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]) => admit | _ => fail end. +Qed. + +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. + +Function plus (m n : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (plus m p) + end. + +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 new file mode 100644 index 0000000..344ee52 --- /dev/null +++ b/mathcomp/ssrtest/elim2.v @@ -0,0 +1,58 @@ +Require Import ssreflect eqtype ssrbool ssrnat seq div fintype finfun path bigop. + +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. +Implicit Arguments big_load [R 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) => admit end. +Ltac ASSERT2 K := match goal with |- (forall x1 : R, R -> + forall y1 : R, R -> K x1 -> K y1 -> K (op x1 y1)) => admit 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)) => admit end. Undo 4. +elim/big_ind2: _ / {-}_. + ASSERT1. ASSERT2 K. match goal with |- (forall i : I, is_true (P i) -> K (F i)) => admit 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)) => admit 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 new file mode 100644 index 0000000..51ab216 --- /dev/null +++ b/mathcomp/ssrtest/elim_pattern.v @@ -0,0 +1,14 @@ +Require Import ssreflect ssrbool eqtype ssrnat. + +Lemma test x : (x == x) = (x + x.+1 == 2 * x + 1). +case: (X in _ = X) / eqP => _. +match goal with |- (x == x) = true => admit end. +match goal with |- (x == x) = false => admit end. +Qed. + +Lemma test1 x : (x == x) = (x + x.+1 == 2 * x + 1). +elim: (x in RHS). +match goal with |- (x == x) = _ => admit end. +match goal with |- forall n, (x == x) = _ -> (x == x) = _ => admit end. +Qed. + diff --git a/mathcomp/ssrtest/first_n.v b/mathcomp/ssrtest/first_n.v new file mode 100644 index 0000000..175684a --- /dev/null +++ b/mathcomp/ssrtest/first_n.v @@ -0,0 +1,9 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect ssrbool. + +Lemma test : False -> (bool -> False -> True -> True) -> True. +move=> F; let w := 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 new file mode 100644 index 0000000..757dba5 --- /dev/null +++ b/mathcomp/ssrtest/gen_have.v @@ -0,0 +1,160 @@ +Require Import ssreflect ssrfun ssrbool eqtype ssrnat. + +Axiom P : nat -> Prop. +Lemma clear_test (b1 b2 : bool) : b2 = b2. +Proof. +(* wlog gH : (b3 := b2) / b2 = b3. admit. *) +gen have {b1} H, gH : (b3 := b2) (w := erefl 3) / b2 = b3. + admit. +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)) => admit end. +Check (lt2le : forall n : nat, 0 < n -> (0 <= n) && (n != 0)). +Check (H1 : 0 <= n). +Check (H2 : n != 0). +admit. +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)) => admit 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). +admit. +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)) => admit end. +Check (H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)). +admit. +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)) => admit end. +move=> H. +Check(H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)). +admit. +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)) => admit end. +move=> H. +Check(H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)). +admit. +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 admit. +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)) => admit end. +Check (H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)). +admit. +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)) => admit end. +Check (H : forall m n : nat, n < m -> (0 <= m) && (m != n)). +admit. +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) => admit end. +Check(n : nat). +Check(m : nat). +Check(z : nat). +Check(ngt0 : z < m). +Check(H : m != 0). +admit. +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. + admit. +Fail Check n. +admit. +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. + admit. +admit. +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) => admit 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) => admit end. +admit. +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}. +admit. +Qed. diff --git a/mathcomp/ssrtest/gen_pattern.v b/mathcomp/ssrtest/gen_pattern.v new file mode 100644 index 0000000..de57e8d --- /dev/null +++ b/mathcomp/ssrtest/gen_pattern.v @@ -0,0 +1,20 @@ +Require Import ssreflect 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 new file mode 100644 index 0000000..3204c42 --- /dev/null +++ b/mathcomp/ssrtest/have_TC.v @@ -0,0 +1,36 @@ +Require Import ssreflect. + +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 admit. +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 admit. +have titi2 : bar _ 5 := . + Fail reflexivity. + by admit. +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 new file mode 100644 index 0000000..f1e3203 --- /dev/null +++ b/mathcomp/ssrtest/have_transp.v @@ -0,0 +1,37 @@ +Require Import ssreflect 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 new file mode 100644 index 0000000..d42a3ac --- /dev/null +++ b/mathcomp/ssrtest/have_view_idiom.v @@ -0,0 +1,6 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect 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 new file mode 100644 index 0000000..c497773 --- /dev/null +++ b/mathcomp/ssrtest/havesuff.v @@ -0,0 +1,73 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import 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 new file mode 100644 index 0000000..619df45 --- /dev/null +++ b/mathcomp/ssrtest/if_isnt.v @@ -0,0 +1,10 @@ +Require Import 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 new file mode 100644 index 0000000..f9d42ff --- /dev/null +++ b/mathcomp/ssrtest/indetLHS.v @@ -0,0 +1,4 @@ +Require Import ssreflect 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 new file mode 100644 index 0000000..6ede976 --- /dev/null +++ b/mathcomp/ssrtest/intro_beta.v @@ -0,0 +1,13 @@ +Require Import 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. +admit. +Qed. diff --git a/mathcomp/ssrtest/intro_noop.v b/mathcomp/ssrtest/intro_noop.v new file mode 100644 index 0000000..91a87b5 --- /dev/null +++ b/mathcomp/ssrtest/intro_noop.v @@ -0,0 +1,23 @@ +Require Import ssreflect ssrbool. + +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 admit. +move: a. +case: b => -[] //. +by admit. +Qed. diff --git a/mathcomp/ssrtest/ipatalternation.v b/mathcomp/ssrtest/ipatalternation.v new file mode 100644 index 0000000..9796648 --- /dev/null +++ b/mathcomp/ssrtest/ipatalternation.v @@ -0,0 +1,6 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import 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 new file mode 100644 index 0000000..3ed274d --- /dev/null +++ b/mathcomp/ssrtest/ltac_have.v @@ -0,0 +1,28 @@ +Require Import ssreflect 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 new file mode 100644 index 0000000..c9f15dd --- /dev/null +++ b/mathcomp/ssrtest/ltac_in.v @@ -0,0 +1,14 @@ +Require Import ssreflect 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 new file mode 100644 index 0000000..9289193 --- /dev/null +++ b/mathcomp/ssrtest/move_after.v @@ -0,0 +1,6 @@ +Require Import 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 new file mode 100644 index 0000000..53b3b4e --- /dev/null +++ b/mathcomp/ssrtest/multiview.v @@ -0,0 +1,56 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect 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. + +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 new file mode 100644 index 0000000..deaee0c --- /dev/null +++ b/mathcomp/ssrtest/occarrow.v @@ -0,0 +1,12 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect 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 new file mode 100644 index 0000000..9cde676 --- /dev/null +++ b/mathcomp/ssrtest/patnoX.v @@ -0,0 +1,5 @@ +Require Import ssreflect ssrbool. +Goal forall x, x && true = x. +move=> x. +Fail (rewrite [X in _ && _]andbT). +Abort. diff --git a/mathcomp/ssrtest/rewpatterns.v b/mathcomp/ssrtest/rewpatterns.v new file mode 100644 index 0000000..88c2a2f --- /dev/null +++ b/mathcomp/ssrtest/rewpatterns.v @@ -0,0 +1,181 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) + +Require Import ssreflect 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. + +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 _ _]]. +admit. +admit. +Qed. + +Goal (exists x : 'I_3, x > 0). +apply: (ex_intro _ (@Ordinal _ 2 _)). +admit. +Qed. + +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 _). +by admit. +Qed. + +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 new file mode 100644 index 0000000..51b8e61 --- /dev/null +++ b/mathcomp/ssrtest/set_lamda.v @@ -0,0 +1,14 @@ +Require Import ssreflect 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 new file mode 100644 index 0000000..0a98267 --- /dev/null +++ b/mathcomp/ssrtest/set_pattern.v @@ -0,0 +1,52 @@ +Require Import ssreflect. + +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. + +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 admit. +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 new file mode 100644 index 0000000..64e78da --- /dev/null +++ b/mathcomp/ssrtest/ssrsyntax1.v @@ -0,0 +1,25 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require 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 new file mode 100644 index 0000000..29985b9 --- /dev/null +++ b/mathcomp/ssrtest/ssrsyntax2.v @@ -0,0 +1,10 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import 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 new file mode 100644 index 0000000..b3f7d3f --- /dev/null +++ b/mathcomp/ssrtest/tc.v @@ -0,0 +1,29 @@ +Require Import 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 new file mode 100644 index 0000000..931cbad --- /dev/null +++ b/mathcomp/ssrtest/testmx.v @@ -0,0 +1,33 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat. +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 new file mode 100644 index 0000000..8ad81a3 --- /dev/null +++ b/mathcomp/ssrtest/typeof.v @@ -0,0 +1,9 @@ +Require Import 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/unkeyed.v b/mathcomp/ssrtest/unkeyed.v new file mode 100644 index 0000000..f6b2021 --- /dev/null +++ b/mathcomp/ssrtest/unkeyed.v @@ -0,0 +1,18 @@ +Require Import ssreflect 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 new file mode 100644 index 0000000..f6de3df --- /dev/null +++ b/mathcomp/ssrtest/view_case.v @@ -0,0 +1,18 @@ +Require Import ssreflect 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 new file mode 100644 index 0000000..4e1c86d --- /dev/null +++ b/mathcomp/ssrtest/wlog_suff.v @@ -0,0 +1,16 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect 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 new file mode 100644 index 0000000..4d20321 --- /dev/null +++ b/mathcomp/ssrtest/wlogletin.v @@ -0,0 +1,37 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect 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 new file mode 100644 index 0000000..97e378a --- /dev/null +++ b/mathcomp/ssrtest/wlong_intro.v @@ -0,0 +1,6 @@ +Require Import ssreflect ssrbool ssrnat. + +Goal (forall x y : nat, True). +move=> x y. +wlog suff: x y / x <= y. +Admitted. |