blob: 11fd7bada72df464aad55f1f29a75afe0433dab8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
|
Require Import Coq.Arith.Arith.
Module A.
Fixpoint foo (n:nat) :=
match n with
| 0 => 0
| S n => bar n
end
with bar (n:nat) :=
match n with
| 0 => 0
| S n => foo n
end.
Lemma using_foo:
forall (n:nat), foo n = 0 /\ bar n = 0.
Proof.
induction n ; split ; auto ;
destruct IHn ; auto.
Qed.
End A.
Module B.
Module A := A.
Import A.
End B.
Module E.
Module B := B.
Import B.A.
(* Bug 1 *)
Lemma test_1:
forall (n:nat), foo n = 0.
Proof.
intros ; destruct n.
reflexivity.
specialize (A.using_foo (S n)) ; intros.
simpl in H.
simpl.
destruct H.
assumption.
Qed.
End E.
|
