aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3350.v
blob: c041c401fd1dbec04caf920a2a448ebc6fec478c (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
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
Require Import TestSuite.admit.
Require Coq.Vectors.Fin.
Require Coq.Vectors.Vector.

Local Generalizable All Variables.
Set Implicit Arguments.

Arguments Fin.F1 : clear implicits.

Lemma fin_0_absurd : notT (Fin.t 0).
Proof. hnf. apply Fin.case0. Qed.

Axiom admit : forall {A}, A.

Fixpoint lower {n:nat} (p:Fin.t (S n)) {struct p} :
  forall (i:Fin.t (S n)), option (Fin.t n)
  := match p in Fin.t (S n1)
           return Fin.t (S n1) -> option (Fin.t n1)
     with
       | @Fin.F1 n1 =>
         fun (i:Fin.t (S n1)) =>
           match i in Fin.t (S n2) return option (Fin.t n2) with
             | @Fin.F1 n2 => None
             | @Fin.FS n2 i2 => Some i2
           end
       | @Fin.FS n1 p1 =>
         fun (i:Fin.t (S n1)) =>
           match i in Fin.t (S n2) return Fin.t n2 -> option (Fin.t n2) with
             | @Fin.F1 n2 =>
               match n2 as n3 return Fin.t n3 -> option (Fin.t n3) with
                 | 0 => fun p2 => False_rect _ (fin_0_absurd p2)
                 | S n3 => fun p2 => Some (Fin.F1 n3)
               end
             | @Fin.FS n2 i2 =>
               match n2 as n3 return Fin.t n3 -> Fin.t n3 -> option (Fin.t n3) with
                 | 0 => fun i3 p3 => False_rect _ (fin_0_absurd p3)
                 | S n3 => fun (i3 p3:Fin.t (S n3)) =>
                             option_map (@Fin.FS _) admit
               end i2
           end p1
     end.

Lemma lower_ind (P: forall n (p i:Fin.t (S n)), option (Fin.t n) -> Prop)
      (c11 : forall n, P n (Fin.F1 n) (Fin.F1 n) None)
      (c1S : forall n (i:Fin.t n), P n (Fin.F1 n) (Fin.FS i) (Some i))
      (cS1 : forall n (p:Fin.t (S n)),
               P (S n) (Fin.FS p) (Fin.F1 (S n)) (Some (Fin.F1 n)))
      (cSSS : forall n (p i:Fin.t (S n)) (i':Fin.t n)
                     (Elow:lower p i = Some i'),
                P n p i (Some i') ->
                P (S n) (Fin.FS p) (Fin.FS i) (Some (Fin.FS i')))
      (cSSN : forall n (p i:Fin.t (S n))
                (Elow:lower p i = None),
                P n p i None ->
                P (S n) (Fin.FS p) (Fin.FS i) None) :
  forall n (p i:Fin.t (S n)), P n p i (lower p i).
Proof.
  fix 2. intros n p.
  refine (match p as p1 in Fin.t (S n1)
                return forall (i1:Fin.t (S n1)), P n1 p1 i1 (lower p1 i1)
          with
            | @Fin.F1 n1 => _
            | @Fin.FS n1 p1 => _
          end); clear n p.
  { revert n1. refine (@Fin.caseS _ _ _); cbn; intros.
    apply c11. apply c1S. }
  { intros i1. revert p1.
    pattern n1, i1; refine (@Fin.caseS _ _ _ _ _);
    clear n1 i1;
    (intros [|n] i; [refine (False_rect _ (fin_0_absurd i)) | cbn ]).
    { apply cS1. }
    { intros p. pose proof (admit : P n p i (lower p i)) as H.
      destruct (lower p i) eqn:E.
      { admit; assumption. }
      { cbn. apply admit; assumption. } } }
Qed.

Section squeeze.
  Context {A:Type} (x:A).
  Notation vec := (Vector.t A).

  Fixpoint squeeze {n} (v:vec n) (i:Fin.t (S n)) {struct i} : vec (S n) :=
    match i in Fin.t (S _n) return vec _n -> vec (S _n)
    with
      | @Fin.F1 n' => fun v' => Vector.cons _ x _ v'
      | @Fin.FS n' i' =>
        fun v' =>
          match n' as _n return vec _n -> Fin.t _n -> vec (S _n)
          with
            | 0 => fun u i' => False_rect _ (fin_0_absurd i')
            | S m =>
              fun (u:vec (S m)) =>
                match u in Vector.t _ (S _m)
                      return Fin.t (S _m) -> vec (S (S _m))
                with
                  | Vector.nil _ => tt
                  | Vector.cons _ h _ u' =>
                    fun j' => Vector.cons _ h _ admit (* (squeeze u' j') *)
                end
          end v' i'
    end v.
End squeeze.

Require Import Program.
Lemma squeeze_nth (A:Type) (x:A) (n:nat) (v:Vector.t A n) p i :
  Vector.nth (squeeze x v p) i = match lower p i with
                                   | Some j => Vector.nth v j
                                   | None => x
                                 end.
Proof.
  (* alternatively: [functional induction (lower p i) using lower_ind] *)
  revert v. pattern n, p, i, (lower p i).
  refine (@lower_ind _ _ _ _ _ _ n p i);
    intros; cbn; auto.

  (*** Fails here with "Conversion test raised an anomaly" ***)
  revert v.
  admit.
  admit.
  admit.
Qed.