$=$ n'est pas $\equiv$, et le programme s'en aperçoit

1. L'expression rend false — mesuré. L'égalité structurelle d'OCaml compare les arbres, et ceux de $p\wedge q$ et $q\wedge p$ diffèrent : leurs sous-arbres gauches ne portent pas la même variable. C'est le = syntaxique du cours.

2. L'équivalence est sémantique : elle se lit sur les valuations, pas sur les arbres.

(* Liste sans doublon des variables de f, par ordre de première rencontre.
   Complexité : O(|f| * v) avec v le nombre de variables distinctes. *)
let variables f =
  let rec aux vus = function
    | Var p -> if List.mem p vus then vus else p :: vus
    | Non g -> aux vus g
    | Et (a, b) | Ou (a, b) | Implique (a, b) -> aux (aux vus a) b
  in
  List.rev (aux [] f)

(* Toutes les valuations sur vs, comme listes d'association.
   Il y en a 2^|vs| : la liste est de taille exponentielle, par nature. *)
let rec valuations = function
  | [] -> [[]]
  | p :: reste ->
      List.concat_map (fun l -> [(p, true) :: l; (p, false) :: l])
                      (valuations reste)

(* Vrai si f et g ont la même valeur sous TOUTE valuation de leurs variables
   réunies. Précondition : aucune. *)
let equivalentes f g =
  let vs = List.sort_uniq compare (variables f @ variables g) in
  List.for_all
    (fun l ->
       let v p = try List.assoc p l with Not_found -> false in
       evalue v f = evalue v g)
    (valuations vs)

Complexité : $\Theta (2^n)$ valuations, chacune évaluée en $O(|f|+|g|)$ multiplié par le coût de List.assoc, soit $O(n)$. Le total est $O(2^n\cdot n\cdot (|f|+|g|))$ — exponentiel, et le cours le dit : « tester l'équivalence coûte, dans l'état des connaissances, un temps exponentiel ».

La ligne à ne pas manquer est variables f @ variables g. Si l'on n'énumérait que les variables de f, on déclarerait $p$ et $p\wedge q$ équivalentes dès que $q$ n'apparaît pas à gauche — une faute qui ne se voit sur aucun exemple symétrique.

3. Non, et l'écart peut être arbitraire : $p$ et $\neg \neg p$ sont équivalentes, de tailles $1$ et $3$ ; plus généralement $p$ et $2k$ négations devant $p$ ont pour tailles $1$ et $2k+1$. De même $p\vee \neg p$ et $q\vee \neg q$ sont équivalentes (toutes deux tautologiques) sans partager la moindre variable. L'équivalence ne dit rien de la forme. C'est précisément ce qui rend la mise en forme normale utile — et dangereuse : elle change la taille sans changer le sens (exercice 20.10).