From f713e6c195d1de177b43cab7c2902f5160f6af9f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 24 Mar 2017 02:18:53 +0100 Subject: A fix to #5414 (ident bound by ltac names now known for "match"). Also taking into account a name in the return clause and in the indices. Note the double meaning ``bound as a term to match'' and ``binding in the "as" clause'' when the term to match is a variable for all of "match", "if" and "let". --- test-suite/output/Cases.out | 46 +++++++++++++++++++++++++++++++++ test-suite/output/Cases.v | 63 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 109 insertions(+) (limited to 'test-suite/output') diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index f064dfe763..97fa8e2542 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -80,3 +80,49 @@ fun '(D n m p q) => n + m + p + q : J -> nat The command has indeed failed with message: The constructor D (in type J) expects 3 arguments. +lem1 = +fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl + : forall k : nat * nat, k = k +lem2 = +fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl + : forall k : bool, k = k + +Argument scope is [bool_scope] +lem3 = +fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl + : forall k : nat * nat, k = k +1 subgoal + + x : nat + n, n0 := match x + 0 with + | 0 => 0 + | S _ => 0 + end : nat + e, + e0 := match x + 0 as y return (y = y) with + | 0 => eq_refl + | S n => eq_refl + end : x + 0 = x + 0 + n1, n2 := match x with + | 0 => 0 + | S _ => 0 + end : nat + e1, e2 := match x return (x = x) with + | 0 => eq_refl + | S n => eq_refl + end : x = x + ============================ + x + 0 = 0 +1 subgoal + + p : nat + a, + a0 := match eq_refl as y in (_ = e) return (y = y /\ e = e) with + | eq_refl => conj eq_refl eq_refl + end : eq_refl = eq_refl /\ p = p + a1, + a2 := match eq_refl in (_ = e) return (p = p /\ e = e) with + | eq_refl => conj eq_refl eq_refl + end : p = p /\ p = p + ============================ + eq_refl = eq_refl diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 6a4fd007df..17fee3303d 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -121,3 +121,66 @@ Check fun x => let '(D n m p q) := x in n+m+p+q. (* This used to succeed, being interpreted as "let '{{n, m, p}} := ..." *) Fail Check fun x : J => let '{{n, m, _}} p := x in n + m + p. + +(* Test use of idents bound to ltac names in a "match" *) + +Lemma lem1 : forall k, k=k :>nat * nat. +let x := fresh "aa" in +let y := fresh "bb" in +let z := fresh "cc" in +let k := fresh "dd" in +refine (fun k : nat * nat => match k as x return x = x with (y,z) => eq_refl end). +Qed. +Print lem1. + +Lemma lem2 : forall k, k=k :> bool. +let x := fresh "aa" in +let y := fresh "bb" in +let z := fresh "cc" in +let k := fresh "dd" in +refine (fun k => if k as x return x = x then eq_refl else eq_refl). +Qed. +Print lem2. + +Lemma lem3 : forall k, k=k :>nat * nat. +let x := fresh "aa" in +let y := fresh "bb" in +let z := fresh "cc" in +let k := fresh "dd" in +refine (fun k : nat * nat => let (y,z) as x return x = x := k in eq_refl). +Qed. +Print lem3. + +Lemma lem4 x : x+0=0. +match goal with |- ?y = _ => pose (match y with 0 => 0 | S n => 0 end) end. +match goal with |- ?y = _ => pose (match y as y with 0 => 0 | S n => 0 end) end. +match goal with |- ?y = _ => pose (match y as y return y=y with 0 => eq_refl | S n => eq_refl end) end. +match goal with |- ?y = _ => pose (match y return y=y with 0 => eq_refl | S n => eq_refl end) end. +match goal with |- ?y + _ = _ => pose (match y with 0 => 0 | S n => 0 end) end. +match goal with |- ?y + _ = _ => pose (match y as y with 0 => 0 | S n => 0 end) end. +match goal with |- ?y + _ = _ => pose (match y as y return y=y with 0 => eq_refl | S n => eq_refl end) end. +match goal with |- ?y + _ = _ => pose (match y return y=y with 0 => eq_refl | S n => eq_refl end) end. +Show. + +Lemma lem5 (p:nat) : eq_refl p = eq_refl p. +let y := fresh "n" in (* Checking that y is hidden *) + let z := fresh "e" in (* Checking that z is hidden *) + match goal with + |- ?y = _ => pose (match y as y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end) + end. +let y := fresh "n" in + let z := fresh "e" in + match goal with + |- ?y = _ => pose (match y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end) + end. +let y := fresh "n" in + let z := fresh "e" in + match goal with + |- eq_refl ?y = _ => pose (match eq_refl y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end) + end. +let p := fresh "p" in + let z := fresh "e" in + match goal with + |- eq_refl ?p = _ => pose (match eq_refl p in _ = z return p=p /\ z=z with eq_refl => conj eq_refl eq_refl end) + end. +Show. -- cgit v1.2.3 From 27c8e30fad95d887b698b0e3fa563644c293b033 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Thu, 23 Jun 2016 15:07:02 +0200 Subject: Prelude : no more autoload of plugins extraction and recdef The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted. --- test-suite/output/Extraction_matchs_2413.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'test-suite/output') diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v index 6c514b16ee..1ecd9771eb 100644 --- a/test-suite/output/Extraction_matchs_2413.v +++ b/test-suite/output/Extraction_matchs_2413.v @@ -1,5 +1,7 @@ (** Extraction : tests of optimizations of pattern matching *) +Require Coq.extraction.Extraction. + (** First, a few basic tests *) Definition test1 b := -- cgit v1.2.3