0
$\begingroup$

I make such codes, and cannot preceed.

From mathcomp Require Import all_ssreflect.

Require Import QArith.

Example example (f : Q -> bool) : 
f 0 = false -> f 1 = true -> 
exists g h : nat -> Q, 
(g 0%nat = 0 /\ h 0%nat = 1) /\
(forall n : nat, 
  if (f ((g n%nat + h n%nat)/2))
    then (g (n+1)%nat = g n%nat /\ 
          h (n+1)%nat = ((g n%nat + h n%nat)/2))
    else (g (n+1)%nat = ((g n%nat + h n%nat)/2) /\
          h (n+1)%nat = h n%nat) ).
Proof.
intros.

(With Pierre Castéran's advice, I try to execute the following code.)

Fix g (n: nat) : Q :=
    match n with
      0% nat => 0
    | S p => if (f ((g p + h p) /2))
             then g p
             else (g p + h p)/2
    end
  with h (n:nat) : Q :=
         match n with
           0% nat => 1
         | S p => if (f ((g p + h p) /2))
                  then (g p + h p)/2
                  else  h p
         end.

The last code tells me that Syntax error.

$\endgroup$

2 Answers 2

4
$\begingroup$

You may define gand hby mutual recursion

Section Example.

  Variables (f : Q -> bool)
    (f0 :  f 0 = false)
    (f1 : f 1 = true). 

 Fixpoint g (n: nat) : Q :=
    match n with
      0% nat => 0
    | S p => if (f ((g p + h p) /2))
             then g p
             else (g p + h p)/2
    end
  with h (n:nat) : Q :=
         match n with
           0% nat => 1
         | S p => if (f ((g p + h p) /2))
                  then (g p + h p)/2
                  else  h p
         end.

In your example, it's even simpler to use a helper:

 Fixpoint gh (n:nat) : Q * Q :=
    match n with
    | 0%nat => (0, 1)
    | S p => match gh p with
                (gp, hp) => let middle := (gp + hp)/2
                            in if (f middle)
                               then (gp, middle)
                               else (middle, hp)
              end
    end.

Then the proof of your lemma may start with:

Proof.
 exists (fun x => fst (gh x)), (fun x => snd (gh x)) .
  simpl.  
$\endgroup$
3
  • $\begingroup$ Can I define Fixpoint in Proof? $\endgroup$ Aug 17 at 9:42
  • $\begingroup$ In interactive proof-mode, you may define mutually recursive functions with fix ... with .... In practice, I prefer using the Section mechanism, with local definitions of gand h, proving technical lemmas that may make the proof of your lemma easier, etc... $\endgroup$ Aug 17 at 10:42
  • $\begingroup$ I'm a beginner in Coq. As you said, after "Proof. Intros." I try to write fix ... with ... However, It tells me Syntax error. How to make it correct? $\endgroup$ Aug 18 at 4:47
2
$\begingroup$

I'm not used to define functions in proof mode, but it's possible.

Lemma L:          
 exists g h : nat -> Q, 
 (g 0%nat = 0 /\ h 0%nat = 1) /\
 (forall n : nat, 
  if (f ((g n%nat + h n%nat)/2))
    then (g (n+1)%nat = g n%nat /\ 
          h (n+1)%nat = ((g n%nat + h n%nat)/2))
    else (g (n+1)%nat = ((g n%nat + h n%nat)/2) /\
          h (n+1)%nat = h n%nat) ).
Proof.
  pose  gh := (fix  gh  (n:nat) : (Q * Q) :=
                   match n with
                     0%nat => (0, 1)
                   |  S p => match gh p with
                               (gp, hp) => let middle := (gp + hp)/2
                                           in if (f middle)
                                              then (gp, middle)
                                              else (middle, hp)
                             end
                   end).
    exists (fun x => fst (gh x)), (fun x => snd (gh x)) .
(* ... *) 

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.